Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic
TR-2005-59, Authors: Rasmus Ejlers Møgelberg, Lars Birkedal and Giuseppe Rosolini Rasmus Ejlers Møgelberg Lars Birkedal Giuseppe Rosolini
In a recent article the first two authors and R.L. Petersen have defined a notion of parametric LAPL-structure. Such structures are parametric models of the equational theory PILLY, a polymorphic intuitionistic / linear type theory with fixed points, in which one can reason using parametricity and, for example, solve a large class of domain equations.
Based on recent work by Simpson and Rosolini we construct a family of parametric LAPL-structures using synthetic domain theory and use the results of Simpson and Rosolini and results about LAPL-structures to prove operational consequences of parametricity for a strict version of the Lily programming language.
In particular we can show that one can solve domain equations in the strict version of Lily up to ground contextual equivalence.
Technical report TR-2005-59
in IT University Technical Report Series
Available as PDF