The semantics of PASCAL in LCF
- Title:
- The semantics of PASCAL in LCF
- Author:
- Aiello, Luigia, Aiello, Mario, and Weyhrauch, Richard W.
- Author (no Collectors):
- Aiello, Luigia, Aiello, Mario, and Weyhrauch, Richard W.
- Collector:
- Aiello, Luigia, Aiello, Mario, and Weyhrauch, Richard W.
- Description:
- We define a semantics for the arithmetic part of PASCAL by giving it an interpretation in LCF, a language based on the typed $\lambda$-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.
- Topic:
- Computer science
- Subject:
- Stanford University. Computer Science Department
- Language:
- English
- Physical Description:
- 1 text file
- Publication Info:
- cau and Stanford (Calif.)
- Date:
- August 1, 1974
- Place created:
- Stanford (Calif.)
- Imprint:
- Stanford (Calif.), August 1, 1974
- Genre:
- technical reports
- Identifier:
- CS-TR-1974-447
- Repository:
- Stanford University. Libraries. Department of Special Collections and University Archives
- Collection:
- Stanford University, Department of Computer Science, Technical Reports and Stanford Artificial Intelligence Laboratory records, 1963-2009
- Manuscript number:
- 3840/2