Title: Possible World Semantics for Impredicative Polymorphism, References,
      and Recursive Types

Speaker: Lars Birkedal
Joint work with: Kristian Stovring, Jacob Thamsborg

We present a possible world semantics for a call-by-value higher-order
programming language with impredicative polymorphism, general references,
and recursive types. The model appears to be the first relationally
parametric model of programming language with all these features.  To model
impredicative polymorphism we define the semantics of types via
parameterized (world-indexed) logical relations over a universal domain. It
is well-known that it is non-trivial to show the existence of logical
relations in the presence of recursive types [Pitts:96].  Here the problems
are exacerbated because of general references.  We explain what the
problems are and present our solution, which makes use of a novel approach
to modeling references.  We prove that the resulting semantics is adequate
with respect to a standard operational semantics and include a simple
example of reasoning about contextual equivalence via parametricity.