parametricity and local variables

To: types
Subject: parametricity and local variables
From: Robert Tennent <rdt@dcs.ed.ac.uk>
Date: Thu, 16 Jul 92 13:39:25 EDT
Sender: meyer@theory.lcs.mit.edu
Date: Thu, 16 Jul 92 13:30:43 BST
Return-Path: <rdt@dcs.ed.ac.uk>

The following manuscript is available (as RPLV.dvi or RPLV.ps)
by anonymous ftp from directory pub/rdt at ftp.dcs.ed.ac.uk : 

         Relational Parametricity and Local Variables
                   (Preliminary Report)

                      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 representations, and demonstrated 
that logical relations could be used 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 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.
--------------------------------------------------------------
Also available (as SLV.dvi or SLV.ps) is the following
expository paper:

@incollection{OHearnTennent92,
	author="P. W. O'Hearn and R. D. Tennent",
	title="Semantics of Local Variables",
	booktitle="Applications of Categories in Computer Science",
	editor="M. P. Fourman and P. T. Johnstone and A. M. Pitts",
	year="1992",
	pages="217-238",
        publisher="Cambridge University Press",
	series="London Mathematical Society Lecture Note Series",
	volume="177",
	address="Cambridge"
}