Copenhagen Programming Language Seminar

The Marriage of Bisimulations and Kripke Logical Relations

Derek Dreyer
Max Planck Institute for Software Systems, Saarbrücken, Germany

December 9th, 2011, 12:00 - 13:00
DIKU, Universitetsparken 1, Room 3-1-25


There has been great progress in recent years on developing effective techniques for reasoning about program equivalence in ML-like languages---that is, languages that combine features like higher-order functions, recursive types, abstract types, and general mutable references. Two of the most prominent types of techniques to have emerged are *bisimulations* and *Kripke logical relations (KLRs)*. While both approaches are powerful, their complementary advantages have led us and other researchers to wonder whether there is an essential tradeoff between them. Furthermore, both approaches seem to suffer from fundamental limitations if one is interested in scaling them to inter-language reasoning.

In this work, we propose *relation transition systems (RTSs)*, which marry together some of the most appealing aspects of KLRs and bisimulations. In particular, RTSs show how bisimulations' support for reasoning about recursive features via *coinduction* can be synthesized with KLRs' support for reasoning about local state via *state transition systems*. Moreover, we have designed RTSs to avoid the limitations of KLRs and bisimulations that preclude their generalization to inter-language reasoning. Notably, unlike KLRs, RTSs are transitively composable.

This is joint work with Gil Hur, Georg Neis, and Viktor Vafeiadis.

Scientific host: Fritz Henglein Administrative host:Jette Møller. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, DTU, ITU, and RUC.
COPLAS is part of the FIRST Research 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