The semantics of PASCAL in LCF.

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