Category-theoretic models of linear Abadi & Plotkin Logic.

Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen

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

Abstract

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
Volume20
Issue number7
Pages (from-to)116-151
Number of pages35
ISSN1201-561X
Publication statusPublished - 2008

Cite this