Program equivalence in a simple language with state

We examine different approaches to reasoning about program equivalence in a higher-order language which incorporates a basic notion of state: references of unit type (names). In particular, we present three such methods stemming from logical relations, bisimulation techniques and game semantics respectively. The methods are tested against a surprisingly difficult example equivalence at second order which exploits the intricacies of the language with respect to privacy and flow of names, and the ensuing notion of local state.

► Proving program equivalences in a language with a minimal local state effect.
► Crash course on logical relations, environmental bisimulations and game semantics.
► Rectification of a proof in nominal game semantics from 2004.