Publication year

LCF considered as a programming language

Resource type
Author/contributor
Title
LCF considered as a programming language
Abstract
The paper studies connections between denotational and operational semantics for a simple programming language based on LCF. It begins with the connection between the behaviour of a program and its denotation. It turns out that a program denotes ⊥ in any of several possible semantics if it does not terminate. From this it follows that if two terms have the same denotation in one of these semantics, they have the same behaviour in all contexts. The converse fails for all the semantics. If, however, the language is extended to allow certain parallel facilities behavioural equivalence does coincide with denotational equivalence in one of the semantics considered, which may therefore be called “fully abstract”. Next a connection is given which actually determines the semantics up to isomorphism from the behaviour alone. Conversely, by allowing further parallel facilities, every r.e. element of the fully abstract semantics becomes definable, thus characterising the programming language, up to interdefinability, from the set of r.e. elements of the domains of the semantics.
Publication
Theoretical Computer Science
Volume
5
Issue
3
Pages
223-255
Date
December 1, 1977
Journal Abbr
Theoretical Computer Science
Language
en
DOI
10/dc7fdn
ISSN
0304-3975
Accessed
2019-11-26T16:59:50Z
Library Catalog
ScienceDirect
Extra
ZSCC: 0001407
Citation
Plotkin, G. D. (1977). LCF considered as a programming language. Theoretical Computer Science, 5(3), 223–255. https://doi.org/10/dc7fdn
Processing time: 0.02 seconds

Graph of references

(from Zotero to Gephi via Zotnet with this script)
Graph of references