Categorical models for Abadi and Plotkin's logic for parametricity

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

We propose a new category-theoretic formulation of relational parametricity based on a logic for reasoning about parametricity given by Abadi and Plotkin (Plotkin and Abadi 1993). 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.

Original languageEnglish
JournalMathematical Structures in Computer Science
Pages (from-to)709-772
Number of pages64
Publication statusPublished - Aug 2005
Externally publishedYes

See relations at Aarhus University Citationformats

ID: 93223462