The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
The Semantics of PASCAL in LCF
The work
| Authors | Luigia Carlucci Aiello; Mario Aiello; Richard W. Weyhrauch |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1974 |
| Citekey | aiello1974semantics |
Identifiers
| DOI | 10.21236/ad0787631 |
|---|---|
| OpenAlex | W106052302 |
Access
| Landing page | https://doi.org/10.21236/ad0787631 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
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.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 05:11 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@techreport{aiello1974semantics,
title = {The Semantics of PASCAL in LCF},
author = {Luigia Carlucci Aiello and Mario Aiello and Richard W. Weyhrauch},
year = {1974},
doi = {10.21236/ad0787631},
}
This record lives at https://refs.drheap.org/aiello1974semantics/ and will keep doing so.