Aarhus University Seal / Aarhus Universitets segl

Category-theoretic models of linear Abadi & Plotkin Logic.

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

Standard

Category-theoretic models of linear Abadi & Plotkin Logic. / Birkedal, Lars; Møgelberg, Rasmus Ejlers; Lerchedahl Petersen, Rasmus.

In: Theory and Applications of Categories, Vol. 20, No. 7, 2008, p. 116-151.

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

Harvard

Birkedal, L, Møgelberg, RE & Lerchedahl Petersen, R 2008, 'Category-theoretic models of linear Abadi & Plotkin Logic.', Theory and Applications of Categories, vol. 20, no. 7, pp. 116-151.

APA

Birkedal, L., Møgelberg, R. E., & Lerchedahl Petersen, R. (2008). Category-theoretic models of linear Abadi & Plotkin Logic. Theory and Applications of Categories, 20(7), 116-151.

CBE

Birkedal L, Møgelberg RE, Lerchedahl Petersen R. 2008. Category-theoretic models of linear Abadi & Plotkin Logic. Theory and Applications of Categories. 20(7):116-151.

MLA

Birkedal, Lars, Rasmus Ejlers Møgelberg and Rasmus Lerchedahl Petersen. "Category-theoretic models of linear Abadi & Plotkin Logic.". Theory and Applications of Categories. 2008, 20(7). 116-151.

Vancouver

Birkedal L, Møgelberg RE, Lerchedahl Petersen R. Category-theoretic models of linear Abadi & Plotkin Logic. Theory and Applications of Categories. 2008;20(7):116-151.

Author

Birkedal, Lars ; Møgelberg, Rasmus Ejlers ; Lerchedahl Petersen, Rasmus. / Category-theoretic models of linear Abadi & Plotkin Logic. In: Theory and Applications of Categories. 2008 ; Vol. 20, No. 7. pp. 116-151.

Bibtex

@article{5ef05cd4c596423a853868b449873a14,
title = "Category-theoretic models of linear Abadi & Plotkin Logic.",
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 parametricLAPL structures, including Simpson and Rosolini{\textquoteright}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].",
author = "Lars Birkedal and M{\o}gelberg, {Rasmus Ejlers} and {Lerchedahl Petersen}, Rasmus",
note = "Udgives af Mount Allison University",
year = "2008",
language = "English",
volume = "20",
pages = "116--151",
journal = "Theory and Applications of Categories",
issn = "1201-561X",
publisher = "Mount Allison University Department of Mathematics and Science",
number = "7",

}

RIS

TY - JOUR

T1 - Category-theoretic models of linear Abadi & Plotkin Logic.

AU - Birkedal, Lars

AU - Møgelberg, Rasmus Ejlers

AU - Lerchedahl Petersen, Rasmus

N1 - Udgives af Mount Allison University

PY - 2008

Y1 - 2008

N2 - 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 parametricLAPL 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].

AB - 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 parametricLAPL 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].

M3 - Journal article

VL - 20

SP - 116

EP - 151

JO - Theory and Applications of Categories

JF - Theory and Applications of Categories

SN - 1201-561X

IS - 7

ER -