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