Hostname: page-component-78c5997874-g7gxr Total loading time: 0 Render date: 2024-11-06T11:46:22.071Z Has data issue: false hasContentIssue false

Categorical models for Abadi and Plotkin's logic for parametricity

Published online by Cambridge University Press:  15 July 2005

LARS BIRKEDAL
Affiliation:
IT University of Copenhagen, Denmark
RASMUS E. MØGELBERG
Affiliation:
IT University of Copenhagen, Denmark

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 describe a way of constructing parametric models from given models of the second-order lambda calculus.

Type
Paper
Copyright
2005 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)