Categorical Models of Abadi-Plotkin's logic for parametricity

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Abstract

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 we describe a way of constructing parametric models from given
models of the second-order lambda calculus.
Original languageEnglish
JournalMathematical Structures in Computer Science
Volume15
Issue number4
Pages (from-to)709-772
Number of pages64
ISSN0960-1295
Publication statusPublished - 2005

Fingerprint

Dive into the research topics of 'Categorical Models of Abadi-Plotkin's logic for parametricity'. Together they form a unique fingerprint.

Cite this