Category-theoretic models of linear Abadi & Plotkin Logic.

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

  • Lars Birkedal
  • Rasmus Ejlers Møgelberg, Denmark
  • Rasmus Lerchedahl Petersen, United Kingdom
This paper presents a sound and complete category-theoretic notion of models for Linear Abadi & Plotkin Logic [Birkedal et al., 2006], a logic suitable for reasoning about parametricity in combination with recursion. A subclass of these called parametric LAPL structures can be seen as an axiomatization of domain theoretic models of parametric polymorphism, and we show how to solve general (nested) recursive domain equations in these. parametric LAPL structures constitute a general notion of model of parametricity in a setting with recursion. In future papers we will demonstrate this by showing how many different models of parametricity and recursion give rise to parametric
LAPL structures, including Simpson and Rosolini’s set theoretic models [Rosolini and Simpson, 2004], a syntactic model based on Lily [Pitts, 2000, Bierman et al., 2000] and a model based on admissible pers over a reflexive domain [Birkedal et al., 2007].
Original languageEnglish
JournalTheory and Applications of Categories
Pages (from-to)116-151
Number of pages35
Publication statusPublished - 2008
Externally publishedYes

See relations at Aarhus University Citationformats

ID: 73743163