The Semantics of PASCAL in LCF. AIM-221
Description
Creators/Contributors
- Author
- Aiello, Luigia
- Aiello, Mario
- Weyhrauch, Richard
Abstract/Contents
- Abstract
- We define a semantics for the arithmetic part of PASCAL by giving it
- an interpretation in LCF, a language based on the typed λ-calculus.
- Programs are represented in terms of their abstract syntax. We show
- sample proofs, using LCF, of some general properties of PASCAL and
- the correctness of some particular programs. A program implementing
- the McCarthy Airline reservation system is proved correct.
Subjects
- Subject
- Stanford Artificial Intelligence Laboratory
- Memo (Stanford Artificial Intelligence Laboratory)
- Artificial intelligence
- Genre
- Memorandums
Bibliographic information
- Finding Aid
-
- Stanford Artificial Intelligence Laboratory Records (SC1041)
- Memo
- AIM-221
- Repository
- Stanford University. Libraries. Department of Special Collections and University Archives
- Location
- SC1041
- https://purl.stanford.edu/gd461tw3281
Access conditions
- Use and reproduction:
- The materials are open for research use and may be used freely for non-commercial purposes with an attribution. For commercial permission requests, please contact the Stanford University Archives (universityarchives@stanford.edu).