Parametric Domain-theoretic Models of Polymorphic Intuitionistic / Linear Lambda Calculus

We present a formalization of a 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, and conclude that such models have solutions for a wide class of recursive domain equations. Finally, we present a concrete parametric LAPL-structure based on suitable categories of partial equivalence relations over a universal model of the untyped lambda calculus. Key words: Parametric polymorphism, Categorical semantics, domain theory

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen
• Keywords: Concrete Parametric Lapl-structure, ENTCS 2006, Parametric Lapl-structure, Recursive Domain Equations