The Girard-Reynolds isomorphism (second edition)

DOI10.1016/j.tcs.2006.12.042zbMath1111.03014OpenAlexW2095835314MaRDI QIDQ879366

Philip Wadler

Publication date: 11 May 2007

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.12.042

zbMATH Keywords

representation theorempolymorphic lambda calculusSystem Fabstraction theoremCurry-HowardGirard-Reynolds type system

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items

Proof-Relevant Parametricity ⋮ Leibniz equality is isomorphic to Martin-Löf identity, parametrically ⋮ Contracts made manifest ⋮ Controlling Program Extraction in Light Logics ⋮ Proofs for free

Uses Software

• ML
• Nuprl
• Automath

Cites Work

• Extensional models for polymorphism
• Functorial polymorphism
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• The calculus of constructions
• A theory of type polymorphism in programming
• On functors expressible in the polymorphic typed lambda calculus
• Formal parametric polymorphism
• Fundamental concepts in programming languages
• The Girard-Reynolds isomorphism
• Constructive mathematics and computer programming
• The Discrete Objects in the Effective Topos
• Categorical data types in parametric polymorphism
• Parametric polymorphism and operational equivalence
• Introduction to generalized type systems
• The Principal Type-Scheme of an Object in Combinatory Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item