Report Number: CS-TR-74-447
Institution: Stanford University, Department of Computer Science
Title: The semantics of PASCAL in LCF.
Author: Aiello, Luigia
Author: Aiello, Mario
Author: Weyhrauch, Richard W.
Date: August 1974
Abstract: 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.