A Semantic Characterization Of Full Abstraction For Typed Lambda Calculi

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 syntacti...

Full description

Saved in:
Bibliographic Details
Main Author: Mulmuley, K.
Format: Conference Proceeding
Language:English
Subjects:
Aerospace electronics
Calculus
Computer science
Contracts
Mathematical programming
US Department of Defense
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0272-5428
DOI:10.1109/SFCS.1984.715926