Compositional relational reasoning via operational game semantics

We show how to use operational game semantics as a guide to develop relational techniques for establishing contextual equivalences with respect to contexts drawn from a hierarchy of four call-by-value higher-order languages: with either general or ground-type references and with either call/cc or no control operator. In game semantics, differences between the contexts can be captured by the absence or presence of the O-visibility and O-bracketing conditions.

The proposed technique, which we call Kripke normal-form bisimulations, combines insights from normal-form bisimulation and Kripke logical relations with game semantics. In particular, the role of the heap and the name history is abstracted away using Kripke-style world transition systems. The differences between the four kinds of contexts manifest themselves through simple local conditions that can be shown to correspond to O-visibility and O-bracketing, as applicable.

The technique is sound and complete by virtue of correspondence with operational game semantics. Moreover, it sheds a new light on other related developments, such as backtracking and private transitions in Kripke logical relations, which can be related to specific phenomena in game models.