Copenhagen Programming Language Seminar

Relational parametricity for computational effects

Rasmus Ejlers Møgelberg
LFCS, University of Edinburgh

Monday, July 2th, Time: 13:00 - 14:00
IT University of Copenhagen, Rued Langgaards Vej 7, auditorium 3


Relational parametricity, as first defined by Reynolds, is a mathematical formulation of Strachey's principle of parametric polymorphism stating that programs of polymorphic type must be based on a uniform algorithm applicable at all type instantiations. This principle has mainly been investigated in pure functional languages such as the second order lambda calculus, where it has proved to be a powerful principle for establishing abstraction properties and proving equivalence of programs. Relational parametricity also has strong type theoretical properties allowing for polymorphic encodings of various type constructors including general inductive and coinductive types from a small collection of basic type constructors. However, it is known that already in the presence of recursion more advanced type theories and logics are needed for consistency.

In this talk, I shall describe a general theory of relational parametricity in languages with computational effects (such as nontermination, exceptions, side-effects, continuations, etc.). As results of this theory we get nontrivial generalisations of polymorphic type encodings known from the pure case. We will also see how the algebraic operations giving rise to effects (such as exception raising, reading and updating variables, etc) can be given polymorphic types and therefore satisfy a suitable parametricity principle.

This is joint work with Alex Simpson

Scientific host: Thomas Hildebrandt. 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/