Sciweavers

APLAS
2015
ACM

Kripke Open Bisimulation - A Marriage of Game Semantics and Operational Techniques

7 years 11 months ago
Kripke Open Bisimulation - A Marriage of Game Semantics and Operational Techniques
Proving that two programs are contextually equivalent is notoriously hard, particularly for functional languages with references (i.e., local states). Many operational techniques have been designed to prove such equivalences, and stract denotational model, using game semantics, have been built for such languages. In this work, we marry ideas coming from trace semantics, an operational variant of game semantics, and from Kripke logical relations, notably the notion of worlds as transition systems of invariants, to define a new operational technique: Kripke open bisimulations. It is the first framework whose completeness does not rely on any closure by contexts.
Guilhem Jaber, Nicolas Tabareau
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where APLAS
Authors Guilhem Jaber, Nicolas Tabareau
Comments (0)