Domain theoretic models of parametric polymorphism

We present a domain-theoretical model of parametric polymorphism based on admissible per’s over a domain-theoretical model of the untyped lambda calculus. The model is shown to be a model of Abadi & Plotkin’s logic for parametricity, by the construction of an LAPL-structure as defined by the authors in [L. Birkedal, R.E. Møgelberg, R.L. Petersen, Parametric domain-theoretical models of polymorphic intuitionistic/linear lambda calculus, in: M. Escardó, A. Jung, M. Mislove (Eds.), Proceedings of Mathematical Foundations of Programming Semantics 2005, vol. 155, 2005, pp. 191–217; L. Birkedal, R.E. Møgelberg, R.L. Petersen, Category theoretical models of linear Abadi & Plotkin logic, 2006 (submitted for publication)]. This construction gives formal proof of solutions to a large class of recursive domain equations, which we explicate. As an example of a computation in the model, we explicitly describe the natural numbers object obtained using parametricity.

The theory of admissible per’s can be considered a domain theory for (impredicative) polymorphism. By studying various categories of admissible and chain complete per’s and their relations, we discover a picture very similar to that of domain theory.