@article{plotkin_lcf_1977,
title = {{LCF} considered as a programming language},
volume = {5},
issn = {0304-3975},
url = {http://www.sciencedirect.com/science/article/pii/0304397577900445},
doi = {10/dc7fdn},
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.},
language = {en},
number = {3},
urldate = {2019-11-26},
journal = {Theoretical Computer Science},
author = {Plotkin, G. D.},
month = dec,
year = {1977},
note = {ZSCC: 0001407},
keywords = {Probabilistic programming, Programming language theory},
pages = {223--255}
}