TY - JOUR
TI - LCF considered as a programming language
AU - Plotkin, G. D.
T2 - Theoretical Computer Science
AB - 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.
DA - 1977/12/01/
PY - 1977
DO - 10/dc7fdn
DP - ScienceDirect
VL - 5
IS - 3
SP - 223
EP - 255
J2 - Theoretical Computer Science
LA - en
SN - 0304-3975
UR - http://www.sciencedirect.com/science/article/pii/0304397577900445
Y2 - 2019/11/26/16:59:50
KW - Probabilistic programming
KW - Programming language theory
ER -