The Semantics of PASCAL in LCF. AIM-221
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 λ-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 |
---|---|
Date created | 1974-10 |
Creators/Contributors
Author | Aiello, Luigia | |
---|---|---|
Author | Aiello, Mario | |
Author | Weyhrauch, Richard |
Subjects
Subject | Stanford Artificial Intelligence Laboratory |
---|---|
Subject | Memo (Stanford Artificial Intelligence Laboratory) |
Subject | Artificial intelligence |
Genre | Memorandums |
Bibliographic information
Finding Aid | |
---|---|
Memo | AIM-221 |
Location | https://purl.stanford.edu/gd461tw3281 |
Location | SC1041 |
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).
- Copyright
- Copyright © The Board of Trustees of the Leland Stanford Junior University. All rights reserved.
Collection
Stanford Artificial Intelligence Laboratory records, 1963-2009
View other items in this collection in SearchWorksAlso listed in
Loading usage metrics...