Lambda the Ultimate

A teaser from POPL'07: A Complete, Co-Inductive Syntactic Theory of Sequential Control and State by Støvring and Lassen.

We present a new 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.