PUMA
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.
 
 
Abstract
(English)
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.
Subject


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