Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic
TR-2005-57, Authors: Rasmus Ejlers Møgelberg, Lars Birkedal and Rasmus Lerchedahl Petersen
Rasmus Ejlers Møgelberg Lars Birkedal Rasmus Lerchedahl Petersen
February 2005
Abstract
We present a formalization of a linear version of Abadi and Plotkin's logic for parametricity for a polymorphic dual intuitionistic / linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a wide collection of types, including solutions to recursive domain equations.
We further define a notion of parametric LAPL-structure and prove that it provides a sound and complete class of models for the logic.
Finally, we present a concrete parametric parametric LAPL-structure based on suitable categories of partial equivalence relations over a universal model of the untyped lambda calculus.
Technical report
TR-2005-57 in
IT University Technical Report Series,
February 2005.
Available as
PDF.