The History of Artificial Intelligence

# The semantics of PASCAL in LCF.

purl.stanford.edu/bx699pp9793
Title:
The semantics of PASCAL in LCF.
Author:
Aiello, Luigia, Aiello, Mario, and Weyhrauch, Richard W.
Author (no Collectors):
Aiello, Luigia, Aiello, Mario, and Weyhrauch, Richard W.
Description:
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.
Topic:
Computer science
Subject:
Stanford University. Computer Science Department
Language:
English
Physical Description:
1 text file
Publication Info:
cau and Stanford (Calif.)
Date:
August 01, 1974
Place created:
Stanford (Calif.)
Imprint:
Stanford (Calif.), August 1, 1974
Genre:
technical reports
Identifier:
CS-TR-1974-447
Repository:
Stanford University. Libraries. Department of Special Collections and University Archives
Collection:
Stanford University, Department of Computer Science, Technical Reports and Stanford Artificial Intelligence Laboratory records, 1963-2009
Manuscript number:
3840/2