Kripke open bisimulation: A marriage of game semantics and operational techniques

Abstract

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 fully abstract 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.