2013 IEEE 54th Annual Symposium on Foundations of Computer Science (1984)
Singer Island, FL
Oct. 24, 1984 to Oct. 26, 1984
K. Mulmuley , Carnegie-Mellon University
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.
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