The marriage of bisimulations and Kripke logical relations

CK Hur, D Dreyer, G Neis, V Vafeiadis (POPL 2012). The marriage of bisimulations and Kripke logical relations.
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 paper, 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.

I understand the paper as offering an extension to bisimulation that handles the notion of hidden transitions properly and so allows a generalisation of KLRs to any systems that can be treated using bisimulations. Applications to verified compilation are mentioned, and everything has been validated in Coq.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

This is a pretty dense paper... tackles a very hard problem in a very general way, and so is full of a lot of technical detail. Unless you're really into the semantics of higher-order imperative programs, it is likely to be quite a difficult read.

Luckily, the same authors wrote a follow-up paper for POPL 2013, The Power of Parameterization in Coinductive Proof, which explains the central technical insight (using Mendler-style corecursion in coinductive proofs) on its own. This is simple and beautiful, and IMO both accessible and widely applicable.

The paper is very

The paper is very contemporary but also an exercise in Model/Lattice theory. For even more basic background I think I see Los' Theorem and compactness in the shadows.