Modular Bisimulation Theory for Computations and Values

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 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]