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

**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} }