Sciweavers

Share
POPL
2012
ACM

The marriage of bisimulations and Kripke logical relations

7 years 11 months ago
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 rder 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 ...
Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Va
Added 25 Apr 2012
Updated 25 Apr 2012
Type Journal
Year 2012
Where POPL
Authors Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis
Comments (0)
books