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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/74/447/CS-TR-74-447.pdf