The Semantics of PASCAL in LCF
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
The authors 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. The authors 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.
- Computer Programming and Software