The Girard-Reynolds isomorphism (second edition)

DOI10.1016/J.TCS.2006.12.042zbMATH Open1111.03014OpenAlexW2095835314MaRDI QIDQ879366FDOQ879366

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

Recommendations

• scientific article; zbMATH DE number 2242602
• The Girard-Reynolds isomorphism
• scientific article
• scientific article
• Polymorphic lambda calculus: The Church-Rosser property

zbMATH Keywords

representation theoremSystem Fabstraction theoremCurry-HowardGirard-Reynolds type systempolymorphic lambda calculus

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (7)

• Title not available (Why is that?)
• Leibniz equality is isomorphic to Martin-Löf identity, parametrically
• The Girard-Reynolds isomorphism
• Contracts made manifest
• Proofs for free. Parametricity for dependent types
• Proof-Relevant Parametricity
• Controlling Program Extraction in Light Logics

Uses Software

• ML
• Nuprl
• Automath

This page was built for publication: The Girard-Reynolds isomorphism (second edition)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q879366)