Accession Number:

AD0787631

Title:

The Semantics of PASCAL in LCF

Descriptive Note:

Technical rept.

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Report Date:

1974-08-01

Pagination or Media Count:

80.0

Abstract:

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE