A Complete, Co-Inductive Syntactic Theory of Sequential Control and State


We present a co-inductive syntactic theory, eager normal form bisimilarity, for the untyped call-by-value lambda calculus extended with continuations and mutable references. We demonstrate that the associated bisimulation proof principle is easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs. The theory is modular in the sense that eager normal form bisimilarity for each of the calculi extended with continuations and/or mutable references is a fully abstract extension of eager normal form bisimilarity for its sub-calculi. For each calculus, we prove that eager normal form bisimilarity is a congruence and is sound with respect to contextual equivalence. Furthermore, for the calculus with both continuations and mutable references, we show that eager normal form bisimilarity is complete: it coincides with contextual equivalence. Eager normal form bisimilarity is inspired by Böhm-tree equivalence in the pure lambda calculus. We clarify the associated proof principle by reviewing properties of Böhm trees and surveying previous work on normal form bisimulation.

Extended version of an earlier conference paper, incorporating parts of Chapter 2 of the first author’s PhD dissertation.