Paper: Reflexive graphs and parametric polymorphism (at LICS 1994)

Authors: Edmund P. Robinson Giuseppe Rosolini

Abstract

The pioneering work on relational parametricity for the second order lambda calculus was done by Reynolds (1983) under the assumption of the existence of set-based models, and subsequently reformulated by him, in conjunction with his student Ma, using the technology of PL-categories. The aim of this paper is to use the different technology of internal category theory to re-examine Ma and Reynolds' definitions. Apart from clarifying some of their constructions, this view enables us to prove that if we start with a non-parametric model which is left exact and which satisfies a completeness condition corresponding to Ma and Reynolds “suitability for polymorphism”, then we can recover a parametric model with the same category of closed types. This implies, for example, that any suitably complete model (such as the PER model) has a parametric counterpart

BibTeX

  @InProceedings{RobinsonRosolini-Reflexivegraphsandp,
    author = 	 {Edmund P. Robinson and Giuseppe Rosolini},
    title = 	 {Reflexive graphs and parametric polymorphism},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {364--371},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }