The semantics of PASCAL in LCF.
Abstract/Contents
- Abstract
- 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.
Description
Type of resource | text |
---|---|
Form | technical reports |
Extent | 1 text file |
Place | Stanford (Calif.) |
Date created | August 1, 1974 |
Language | English |
Digital origin | reformatted digital |
Creators/Contributors
Author | Aiello, Luigia | |
---|---|---|
Author | Aiello, Mario | |
Author | Weyhrauch, Richard W. |
Subjects
Subject | Stanford University. Computer Science Department |
---|---|
Subject | Computer science |
Genre | Technical reports |
Bibliographic information
Finding Aid | |
---|---|
Technical Report # | CS-TR-1974-447 |
Location | https://purl.stanford.edu/bx699pp9793 |
Location | 3840/2 |
Repository | Stanford University. Libraries. Department of Special Collections and University Archives |
Access conditions
- Use and reproduction
- The materials are open for research use and may be used freely for non-commercial purposes with an attribution. For commercial permission requests, please contact the Stanford University Archives (universityarchives@stanford.edu).
Collection
Stanford University, Department of Computer Science, Technical Reports
View other items in this collection in SearchWorksStanford Artificial Intelligence Laboratory records, 1963-2009
View other items in this collection in SearchWorksAlso listed in
Loading usage metrics...