The Semantics of PASCAL in LCF. AIM-221
- Title:
- The Semantics of PASCAL in LCF. AIM-221
- Author:
- Aiello, Luigia, Aiello, Mario, and Weyhrauch, Richard
- Author (no Collectors):
- Aiello, Luigia, Aiello, Mario, and Weyhrauch, Richard
- Collector:
- Aiello, Luigia, Aiello, Mario, and Weyhrauch, Richard
- Description:
-
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.
- Topic:
- Artificial intelligence
- Subject:
- Stanford Artificial Intelligence Laboratory and Memo (Stanford Artificial Intelligence Laboratory)
- Date:
- 1974-10
- Imprint:
- 1974-10
- Genre:
- memorandums
- Identifier:
- AIM-221
- Repository:
- Stanford University. Libraries. Department of Special Collections and University Archives
- Collection:
- Stanford Artificial Intelligence Laboratory records, 1963-2009
- Manuscript number:
- SC1041