Geodesic
Category-theoretic models of linear Abadi and Plotkin logic
Theory and applications of categories, Tome 20 (2008), pp. 116-151

Voir la notice de l'article provenant de la source Theory and Applications of Categories website

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.

Classification : 03B70, 18C50, 68Q55
Keywords: Parametric polymorphism, categorical semantics, axiomatic domain theory, recursive types, fibrations 
@article{TAC_2008_20_a6,
     author = {Lars Birkedal and Rasmus E. Mogelberg and Rasmus L. Petersen},
     title = {Category-theoretic models of linear {Abadi} and {Plotkin} logic},
     journal = {Theory and applications of categories},
     pages = {116--151},
     publisher = {mathdoc},
     volume = {20},
     year = {2008},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_2008_20_a6/}
}
TY  - JOUR
AU  - Lars Birkedal
AU  - Rasmus E. Mogelberg
AU  - Rasmus L. Petersen
TI  - Category-theoretic models of linear Abadi and Plotkin logic
JO  - Theory and applications of categories
PY  - 2008
SP  - 116
EP  - 151
VL  - 20
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TAC_2008_20_a6/
LA  - en
ID  - TAC_2008_20_a6
ER  - 
%0 Journal Article
%A Lars Birkedal
%A Rasmus E. Mogelberg
%A Rasmus L. Petersen
%T Category-theoretic models of linear Abadi and Plotkin logic
%J Theory and applications of categories
%D 2008
%P 116-151
%V 20
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TAC_2008_20_a6/
%G en
%F TAC_2008_20_a6
Lars Birkedal; Rasmus E. Mogelberg; Rasmus L. Petersen. Category-theoretic models of linear Abadi and Plotkin logic. Theory and applications of categories, Tome 20 (2008), pp. 116-151. http://geodesic.mathdoc.fr/item/TAC_2008_20_a6/