The Semantics of PASCAL in LCF
Luigia Carlucci Aiello, M. Anthony Aiello, Richard W. Weyhrauch · 1974
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.