Wadler's Blog

In a series of papers, published 2001-2007, I explained Reynold's Abstraction Theorem as a mapping from System F to a suitable logic, and Girard's Representation Theorem as a mapping from the logic back into System F, with the two mappings forming an embedding-projection pair.  Recently, Bernardy, Janson, and Paterson have described a lovely generalisation of this idea to an arbitary Pure Type System (PTS).  An illuminating part of their construction is that given one PTS, they can construct another suitable for use as the logic of the first.  The journal version of their work arrived in my postbox this morning.  Neat stuff!

Jean-Philippe Bernardy, Patrik Janson, and Ross Paterson, Proofs for Free: Parametricity for dependent types, Journal of Functional Programming 22(2):107-152, March 2012.

Studies of parametricity for System F and its variants abound in the literature, starting with the seminal paper by Reynolds (1983), where the polymorphic semantics of System F types is captured in a suitable model.
We use here a more syntactic approach, where the expressions of the programming language are (syntactically) translated to formulas describing the program. This style was pioneered by Mairson (1991) and used by a number of authors, including Abadi et al. (1993), Plotkin & Abadi (1993), and Wadler (2007). In particular,Wadler (2007) gives an insightful presentation of the abstraction theorem, as the inverse of Girard’s (1972) Representation theorem: Reynolds (1983) gives an embedding from System F to second-order logic, while Girard (1972) gives the corresponding projection. Our version of the abstraction theorem differs in the following aspects from that of Wadler (2007) (and to our knowledge all others):
1. Instead of targeting a logic, we target its propositions-as-types interpretation, expressed in a PTS.
2. We abstract from the details of the systems, generalising to a class of PTSs.
3. We add that the translation function used to interpret types as relations can also be used to interpret terms as witnesses of those relations.
The question of how Girard’s projection generalises to arbitrary PTSs naturally arises, and is addressed by Bernardy & Lasson (2011).

Philip Wadler (2007), The Girard-Reynolds isomorphism (second edition),   Theoretical Computer Science 375(1-3):201-226.