We present a new normal form bisimulation theory for the untyped call-by-value lambda calculus extended with continuations and mutable references. The associated bisimulation proof principle is sound and complete with respect to contextual equivalence. We demonstrate that this proof principle is furthermore easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs.

Normal form bisimulation is based on symbolic evaluation of open terms to normal forms. It does not involve any universal quantification over function arguments and is therefore, in some respects, a more powerful proof principle for proving equivalences between recursive higher-order functions than other operationally-based syntactic methods.

This work is joint with Soren Lassen; it is to be presented at POPL'07.