This page contains supporting material for Modular Bisimulation Theory for Computations and Values, a paper to be presented at FoSSaCS 2013 by Martin Churchill and Peter Mosses. The DOI is 10.1007/978-3-642-37075-5_7. We have:
- Author’s version of the paper itself [fossacs13]. The final publication is available at springerlink.com, specifically here.
- Proofs of the congruence results for the value-added and MSOS tyft formats [congruence-proofs]
- Examples of modular bisimulations in this framework on paper [bisim-examples]
- Examples of how such bisimulations can be formulated in proof assistants (Coq) [bisim-examples-coq]
- A demonstration that the congruence format is liberal, by providing operational semantics of Caml Light in this rule format [caml-light-dynamics]
- Slides from Martin’s talk at FoSSaCS in Rome on March 18th, 2013 [slides]