Relational Parametricity and Local Variables

Abstract

J. C. Reynolds suggested that Strachey's intuitive concept of “parametric” (i.e., uniform) polymorphism is closely linked to representation independence, and used logical relations to formalize 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, by showing that interactions between local and non-local entities satisfy certain relational criteria.