TY - JOUR

T1 - Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic

AU - Møgelberg, Rasmus Ejlers

AU - Birkedal, Lars

AU - Rosolini, Guiseppe

N1 - Forfatters note: "Annals of Pure and Applied Logic er den korrekte titel på tidsskriftet. Det eksisterer desværre kun under den gamle titel i FIs centrale database."
Korrekt tidskrift tilføjet af validator.
Paper id:: 10.1016/j.apal.2008.03.006

PY - 2008/9/2

Y1 - 2008/9/2

N2 - Plotkin suggested using a polymorphic dual intuitionistic/linear type theory (PILLY) as a metalanguage for parametric polymorphism and recursion. In recent work the first two authors and R.L. Petersen have defined a notion of parametric LAPL-structure, which are models of PILLY, in which one can reason using parametricity and, for example, solve a large class of domain equations, as suggested by Plotkin.In this paper, we show how an interpretation of a strict version of Bierman, Pitts and Russo's language Lily into synthetic domain theory presented by Simpson and Rosolini gives rise to a parametric LAPL-structure. This adds to the evidence that the notion of LAPL-structure is a general notion, suitable for treating many different parametric models, and it provides formal proofs of consequences of parametricity expected to hold for the interpretation. Finally, we show how these results, in combination with Rosolini and Simpson's computational adequacy result, can be used to prove consequences of parametricity for Lily. In particular, we show that one can solve domain equations in Lily up to ground contextual equivalence.

AB - Plotkin suggested using a polymorphic dual intuitionistic/linear type theory (PILLY) as a metalanguage for parametric polymorphism and recursion. In recent work the first two authors and R.L. Petersen have defined a notion of parametric LAPL-structure, which are models of PILLY, in which one can reason using parametricity and, for example, solve a large class of domain equations, as suggested by Plotkin.In this paper, we show how an interpretation of a strict version of Bierman, Pitts and Russo's language Lily into synthetic domain theory presented by Simpson and Rosolini gives rise to a parametric LAPL-structure. This adds to the evidence that the notion of LAPL-structure is a general notion, suitable for treating many different parametric models, and it provides formal proofs of consequences of parametricity expected to hold for the interpretation. Finally, we show how these results, in combination with Rosolini and Simpson's computational adequacy result, can be used to prove consequences of parametricity for Lily. In particular, we show that one can solve domain equations in Lily up to ground contextual equivalence.

M3 - Journal article

SN - 0168-0072

VL - 155

SP - 115

EP - 133

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 2

ER -