Hostname: page-component-74656f9884-8r8nv Total loading time: 0 Render date: 2026-11-09T04:29:44.139Z 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
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

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.

Information

Type
Paper
Copyright
2005 Cambridge University Press