|
Abstract : |
Abstract. Lambda definability is characterized in categorical models of simply typed lambda calculus with type variables. A category-theoretic framework known as glueing or sconing is used to extend the Jung-Tiuryn characterization of lambda definability [JuT93], first to ccc models, and then to categorical models of the calculus with type variables. Logical relations are now a well-established tool for studying the semantics of various typed lambda calculi. The main lines of research are focused in two areas, the first of which strives for an understanding of Strachey's notion of parametric polymorphism. The main idea is that a parametricly polymorphic function acts independently from the types to which its type variables are instantiated, and that this uniformity may be captured by imposing a relational structure on the types [OHT93, MSd93, MaR91, Wad89, Rey83, Str67]. The other line of research concerns lambda definability and the full abstraction problem for various models of languages based on simply typed lambda calculus [JuT93, MaR91, MSd93, OHR94, Pit93, Plo80, Lau70]. Early attempts, |
