TY - RPRT
T1 - On the Definition of Parametricity
AU - Birkedal, Lars
AU - Møgelberg, Rasmus Ejlers
PY - 2004/2
Y1 - 2004/2
N2 - 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.
AB - 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.
KW - category-theoretic formulation
KW - relational parametricity
KW - Abadi and Plotkin logic
KW - parametric models
KW - second-order lambda calculus
M3 - Report
T3 - IT University Technical Report Series
BT - On the Definition of Parametricity
PB - IT-Universitetet i København
CY - Copenhagen
ER -