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.