#
Category-theoretic models of linear Abadi and Plotkin logic

##
Lars Birkedal and Rasmus E. Mogelberg and Rasmus L. Petersen

This paper presents a sound and complete category-theoretic notion
of models for Linear Abadi and Plotkin Logic, 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, a syntactic model based
on Lily and a model based on admissible pers over a reflexive domain.

Keywords:
Parametric polymorphism, categorical semantics, axiomatic
domain theory, recursive types, fibrations

2000 MSC:
03B70, 18C50, 68Q55

*Theory and Applications of Categories,*
Vol. 20, 2008,
No. 7, pp 116-151.

http://www.tac.mta.ca/tac/volumes/20/7/20-07.dvi

http://www.tac.mta.ca/tac/volumes/20/7/20-07.ps

http://www.tac.mta.ca/tac/volumes/20/7/20-07.pdf

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/20/7/20-07.dvi

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/20/7/20-07.ps

TAC Home