Paper: Reflexive graphs and parametric polymorphism (at LICS 1994)
Authors: Edmund Robinson Giuseppe RosoliniAbstract
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 Robinson and Giuseppe Rosolini}, title = {Reflexive graphs and parametric polymorphism}, booktitle = {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994}, year = 1994, editor = {Samson Abramsky}, month = {July}, pages = {364--371}, location = {Paris, France}, publisher = {IEEE Computer Society Press} }