@article{plotkin-1977-lcf,
title = {LCF considered as a programming language},
journal = {Theoretical Computer Science},
volume = {5},
number = {3},
pages = {223-255},
year = {1977},
issn = {0304-3975},
doi = {10.1016/0304-3975(77)90044-5},
url = {https://www.sciencedirect.com/science/article/pii/0304397577900445},
author = {G.D. Plotkin}
}
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”.