[TYPES] Paper announcement: Syntactic Logical Relations for Polymorphic and Recursive Types

[Karl Crary]

I am pleased to announce the availability of the paper "Syntactic 
Logical Relations for Polymorphic and Recursive Types" at the following 
URLs:

http://www.cs.cmu.edu/~crary/papers/2007/relns.pdf
or
http://www.cs.cmu.edu/~rwh/papers/polyrecrelns/gdpfs.pdf

As always, comments are welcome.

Karl Crary (for myself and Robert Harper)

----------

Syntactic Logical Relations for Polymorphic and Recursive Types
Karl Crary and Robert Harper

  The method of logical relations assigns a relational interpretation to 
types
  that expresses operational invariants satisfied by all terms of a 
type.  The
  method is widely used in the study of typed languages, for example to
  establish contextual equivalences of terms.  The chief difficulty in using
  logical relations is to establish the existence of a suitable relational
  interpretation.  We extend work of Pitts and Birkedal and Harper on
  constructing relational interpretations of types to polymorphism and 
recursive
  types, and apply it to establish parametricity and representation 
independence
  properties in a purely operational setting.  We argue that, once the 
existence
  of a relational interpretation has been established, it is 
straightforward to
  use it to establish properties of interest.