2013 IEEE 54th Annual Symposium on Foundations of Computer Science (1984)

Singer Island, FL

Oct. 24, 1984 to Oct. 26, 1984

ISBN: 0-8186-0591-X

pp: 279-288

K. Mulmuley , Carnegie-Mellon University

ABSTRACT

Full abstraction is a well known issue in denotational semantics. For a special case of typed lambda calculus, PCF, Plotkin showed that the classical model consisting of domains of continuous functions is not fully abstract. Milner constructed a fully abstract model of typed lambda calculus syntactically. However, its precise relationship with the classical model was not clear, and hence it remained open whether a fully abstract model can be constructed which is related to the classical model in a pleasant way. In this paper we show that a fully abstract, extensional model of typed lambda calculus can be constructed as a homomorphic retraction of the classical model.

INDEX TERMS

CITATION

K. Mulmuley,
"A Semantic Characterization Of Full Abstraction For Typed Lambda Calculi",

*2013 IEEE 54th Annual Symposium on Foundations of Computer Science*, vol. 00, no. , pp. 279-288, 1984, doi:10.1109/SFCS.1984.715926