[Pl-seminar] 1/19: Derek Dreyer, "The Marriage of Bisimulations and Kripke Logical Relations"

[Aaron Turon]

NEU Programming Languages Seminar presents

Derek Dreyer
MPI-SWS

Thursday, 1/19
1:45pm-3:00pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

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 with regards to their potential
for 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, while avoiding their drawbacks.  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*.

The key technical insight behind RTSs is something we call "global vs.
local knowledge".  The idea is to distinguish one's "local
knowledge" about program equivalence (i.e. the terms whose equivalence
one wishes to prove) from the "global knowledge" (i.e. the relation
defining when unknown higher-order values passed in from the context
are equivalent), and to parameterize the proof of correctness for the
former over the latter.  By *parameterizing over* the global knowledge
instead of attempting to characterize it directly, RTSs 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.