Lambda the Ultimate

A Model for Formal Parametric Polymorphism: A PER Interpretation for System R , Roberto Bellucci, Martin Abadi, Pierre-Louis Curien. TLCA 1995

System R is an extension of system F that formalizes Reynolds' notion of relational parametricity. In system R, considerably more lambda-terms can be proved equal than in system F: for example, the encoded weak products of F are strong products in R. Also, many "theorems for free" à la Wadler can be proved formally in R. In this paper we describe a semantics for system R. As a first step, we give a precise and general reconstruction of the per model of system F of Bainbridge et al., presenting it as a categorical model in the sense of Seely. Then we interpret System R in this model.

System R is a logic for proving relational parametricity results. It's similar in some ways to Abadi-Plotkin logic, which we have linked to previously on LtU.