The Girard-Reynolds Isomorphism

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 propositional 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 embeddingof F2 into P2, and that the Reynolds embeddingfollo wed 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 embeddingshould also be the identity. However, we show that in the presence of Reynolds’s parametricity property that this is indeed the case, for propositions correspondingto inductive definitions of naturals, products, sums, and fixpoint types.
Original languageEnglish
Title of host publicationTheoretical Aspects of Computer Software
Subtitle of host publication4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings
PublisherSpringer Berlin Heidelberg
Pages468-491
Number of pages24
ISBN (Electronic)978-3-540-45500-4
ISBN (Print)978-3-540-42736-0
DOIs
Publication statusPublished - 2001

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume2215
ISSN (Print)0302-9743

Fingerprint

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

Cite this