Relational Parametricity and Local Variables

P W O'Hearn and R D Tennent

Abstract: J C Reynolds has argued that Strachey's intuitive concept of ``parametric'' (i.e. uniform) polymorphism has essentially to do with representation independence in the programming of data representation, and demonstrated that logical relations could be used to formalise this principle in languages with type variables and user-defined types.

Here, we use relational parametricity to address long-standing problems with the semantics of local-variable declarations in Algol-like languages. The new model is based on a cartesian closed category of ``relation-preserving'' functors and natural transformations which is induced by a suitable category of ``possible worlds'' with relations assigned to its objects and morphisms. The semantic interpretation supports straightforward validations of all the test equivalences that have been proposed in the literature; however, it is not known whether it is fully abstract.

LFCS report ECS-LFCS-92-223

A revised version of this paper appeared in the Conference Record of the 20th ACM Symposium on Principles of Programming Languages, Charleston SC, 1993, pp171-184. The paper was subsequently updated as ``Parametricity and Local Variables'' and is to appear in the Journal of the ACM.

Previous | Index | Next