Parametricity and Local Variables

The following paper is available by anonymous ftp from top.cis.syr.edu
in ohearn/plv.dvi

Parametricity and Local Variables
P. W. O'Hearn and R. D. Tennent

We propose that the phenomenon of local state may be understood 
in terms of Strachey's concept of parametric (i.e., uniform) 
polymorphism.  The intuitive basis for our proposal is the following 
analogy: a non-local procedure is independent of locally-declared
variables in the same way that  a parametrically polymorphic function 
is independent of types to which it is instantiated.

A connection between parametricity and representational abstraction
was first suggested by J.\,C.~Reynolds.  Reynolds used logical 
relations to formalize this connection in languages with type 
variables and user-defined types.  We use relational parametricity
to construct a model for an Algol-like language in which interactions 
between local and non-local entities satisfy certain relational 
criteria.  Reasoning about local variables essentially involves 
proving properties of polymorphic functions. The new model supports 
straightforward validations of all the test equivalences that have 
been proposed in the literature for local-variable semantics, 
and encompasses standard methods of reasoning about data 
representations.  It is not known whether our techniques yield fully
abstract semantics.  A model based on partial equivalence relations
on the natural numbers is also briefly examined.

This is an expansion and elaboration of material from
the preliminary report "Relational Parametricity and Local Variables",
which appeared in POPL93.