Proving Equivalence of Programs in a Higher-Order Language with References

Guilhem Jaber

Contextual equivalence of programs written in a functional language with references (i.e. local stores) is a notoriously hard problem, specially with higher-order references (i.e. references which can stores functions). In the last twenty years, different techniques have been introduce to that purpose: Kripke Logical Relations, Bisimulations and Algorithmic Game Semantics.

We first present these techniques, then we introduce Kripke Open Bisimulations (KOS) which combine ideas from them. To prove completeness of KOS, we introduce an operational variant of Game Semantics, namely a Nominal Trace Semantics.

Then, we show how we can automatize reasoning on KOS, using a symbolic execution of the language, together with a temporal logic. A translation of this temporal logic to a SAT solver then allows us to automatically model-check if two programs are equivalent, providing the right invariants on the stores.