A Complete, Co-Inductive Syntactic Theory of Sequential Control and State
Venue
Semantics and Algebraic Specification: Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday, Springer (2009), pp. 329-375
Publication Year
2009
Authors
Kristian Støvring, Soren B. Lassen
BibTeX
Abstract
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.
