Copenhagen Programming Language Seminar

State-Dependent Representation Independence

Derek Dreyer
Max Planck Institute for Software Systems

Monday, September 1, 2008, 11:00-12:00
ITU, Rued Langgaards Vej 7, 2300 Copenhagen S. Room: Auditorium 2A.18


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.

Bio: Derek Dreyer received his Ph.D. in Computer Science from Carnegie Mellon University in 2005. From 2005 to 2007, he was a research assistant professor at the Toyota Technological Institute at Chicago (TTI-C). He is currently tenure-track faculty at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken, Germany, where he heads the Type Systems and Functional Programming group. Derek's research to date has focused on the design of module systems for strongly-typed functional languages. In addition to investigating the type-theoretic foundations of modules, with particular emphasis on the ML module system, he has developed new and more expressive module languages that synthesize such features as higher-order modules, recursive modules, Haskell-style type classes, mixin modules, and type inference. He is also currently investigating techniques for reasoning about the semantics of modular programs.

Scientific host: Lars Birkedal. Administrative host: Annette Enggaard. 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 prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org