On the Definition of Parametricity
TR-2004-44, Authors: L. Birkedal and R. Mogelberg
On the Definition of Parametricity
February 2004
Abstract
We propose a new category-theoretic formulation of relational parametricity based on a logic for reasoning about parametricity given by Abadi and Plotkin. The logic can be used to reason about parametric models, such that we may prove consequences of parametricity that to our knowledge have not been proved before for existing category-theoretic notions of relational parametricity. We provide examples of parametric models and we describe a way of constructing parametric models from given models of the second-order lambda calculus.
Technical report [TR-2004-44] in IT University Technical Report Series, February 2004.
Available as PDF.