Extensional models for polymorphism

DOI10.1016/0304-3975(88)90097-7zbMath0713.03005OpenAlexW2117721239MaRDI QIDQ749518

Val Breazu-Tannen, Thierry Coquand

Publication date: 1988

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://repository.upenn.edu/cgi/viewcontent.cgi?article=1652&context=cis_reports

zbMATH Keywords

extensional models for the Girard-Reynolds polymorphic lambda calculus

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Combinatory logic and lambda calculus (03B40)

Related Items (15)

Algebraic types in PER models ⋮ The Girard-Reynolds isomorphism ⋮ Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus ⋮ Categorical data types in parametric polymorphism ⋮ Polymorphic extensions of simple type structures. With an application to a bar recursive minimization ⋮ The Girard-Reynolds isomorphism (second edition) ⋮ Parametricity of extensionally collapsed term models of polymorphism and their categorical properties ⋮ The calculus of dependent lambda eliminations ⋮ A modest model of records, inheritance, and bounded quantification ⋮ Recursion over realizability structures ⋮ Inheritance as implicit coercion ⋮ Recursive types for Fun ⋮ Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves ⋮ Linear realizability and full completeness for typed lambda-calculi ⋮ Functorial polymorphism

Cites Work

• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• A small complete category
• The lambda calculus, its syntax and semantics
• On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
• Edinburgh LCF. A mechanized logic of computation
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• On the axiom of extensionality – Part I
• λ-definable functionals andβη conversion
• The Discrete Objects in the Effective Topos
• The Expressiveness of Simple and Second-Order Type Structures
• Categorical semantics for higher order polymorphic lambda calculus
• Lambda‐Calculus Models and Extensionality
• Completeness, invariance and λ-definability
• What is a model of the lambda calculus?
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Extensional models for polymorphism