Istituto di Scienza e Tecnologie dell'Informazione     
Aiello L., Aiello M., Weyhrauch R. The semantics of PASCAL in LCF. Apparso in 'Memo AIM-221, Stanford Artificial Intelligence Laboratory', August 1974). Dicembre 1974. Internal note IEI-B74-48, 1974.
We define a semantics for the arithmetic part of PASCAL by giving it an interpretation in LCF, a language based on the typed Ⲗ-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 reservetion system is proved correct.

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional