The Semantics of PASCAL in LCF. AIM-221
- Aiello, Luigia
- Aiello, Mario
- Weyhrauch, Richard
- 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.
- Stanford Artificial Intelligence Laboratory
- Memo (Stanford Artificial Intelligence Laboratory)
- Artificial intelligence
- Finding Aid
- Stanford Artificial Intelligence Laboratory Records (SC1041)
- Stanford University. Libraries. Department of Special Collections and University Archives
- 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 (firstname.lastname@example.org).