Open Access
A Complete, Co-Inductive Syntactic Theory of Sequential Control and State
Author(s) -
Kristian Støvring,
Søren B. Lassen
Publication year - 2007
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v14i4.21927
Subject(s) - bisimulation , equivalence (formal languages) , mathematics , extension (predicate logic) , computer science , algebra over a field , discrete mathematics , pure mathematics , calculus (dental) , programming language , medicine , dentistry
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.