Domain-theoretical 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. Mogelberg, R.L. Petersen, Parametric domain-theoretical models of polymorphic intuitionistic/linear lambda calculus, in: M. Escardo, A. Jung, M. Mislove (Eds.), Proceedings of Mathematical Foundations of Programming Semantics 2005, vol. 155, 2005, pp. 191-217; L. Birkedal, R.E. Mogelberg, 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. (C) 2007 Elsevier B.V. All rights reserved.
parametric polymorphism domain theory realizability models