Copenhagen Programming Language Seminar
Mitchell's notion of representation independence is a particularly useful application of Reynolds' relational parametricity --- two different implementations of an abstract data type can be shown contextually equivalent so long as there exists a relation between their type representations that is preserved by their operations. There have been a number of methods proposed for proving representation independence in pure extensions of System F, as well as in impure Java-like languages. However, none of the existing work on representation independence addresses the interaction of existential type abstraction and mutable state. Specifically, none shows how to prove equivalence of generative ADTs, for which each instance of the ADT must introduce a distinct abstract type because the relational interpretation of that type depends on some local instance-specific state.
In this work, we present a method for proving state-dependent
representation independence. Our method extends Ahmed's previous work
on step-indexed logical relations for recursive and quantified types
in order to handle ML-style unrestricted state. We use this method to
prove a number of interesting contextual equivalences, some drawn from
the literature on type generativity, that involve a close interaction
between existentials and state. In these examples, the relational
interpretations of the abstract types may be initially empty and then
grow over time in a manner that is tightly coupled with changes to
some local state. We encode such state-dependent type representations
using a novel possible-worlds model that is inspired by several recent
approaches but relies on step-indexing to enable a well-founded
quasi-circular definition of possible worlds.
This is joint work with Amal Ahmed and Andreas Rossberg.
All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org