The Girard-Reynolds isomorphism

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

The second-order polymorphic lambda calculus, F2, was independently discovered by Girard and Reynolds. Girard additionally proved a Representation Theorem: every function on natural numbers that can be proved total in second-order intuitionistic predicate logic, P2, can be represented in F2. Reynolds additionally proved an Abstraction Theorem: for a suitable notion of logical relation, every term in F2 takes related arguments into related results. We observe that the essence of Girard?s result is a projection from P2 into F2, and that the essence of Reynolds?s result is an embedding of F2 into P2, and that the Reynolds embedding followed by the Girard projection is the identity. The Girard projection discards all first-order quantifiers, so it seems unreasonable to expect that the Girard projection followed by the Reynolds embedding should also be the identity. However, we show that in the presence of Reynolds?s parametricity property that this is indeed the case, for propositions corresponding to inductive definitions of naturals or other algebraic types.
Original languageEnglish
Pages (from-to)260 - 284
JournalInformation and Computation
Issue number2
Publication statusPublished - 1 Nov 2003


Dive into the research topics of 'The Girard-Reynolds isomorphism'. Together they form a unique fingerprint.

Cite this