This webpage contains some supporting material for the paper:

which will appear in the proceedings of CPP 2015.

You may browse the following development on-line. To run them yourself, you will need version 2.0.2 of Abella, available from the main Abella web-page.

`ccs_core`

contains the core definitions of the labelled transition system of CCS and the definition of bisimulation-up-to. There are also some simple lemmas about ordinary bisimulation (*a.k.a.*bisimulation up to reflexivity).`ccs_bisim`

contains the soundness proof of*bisimulation up to bisimilarity*.`ccs_ctx`

contains the definitions of process contexts and the proof that CCS contexts are faithful.`ccs_context`

contains the soundness proof of*bisimulation up to context*.`ccs_bisim_context`

contains the soundness proof of*bisimulation up to bisimilarity and context*.

Examples

`ccs_bisim_examples_helper`

contains some common lemmas for the examples.`ccs_bisim_examples`

and`ccs_bisim_context_examples`

contain some examples of the use of the up-to-bisimilarity technique to show the bisimilarity of processes that have only infinite bisimulations.

Package

`ccs.tar.gz`

, which packages up the above files together with a`Makefile`

to run the sources through Abella in the right order.

`pic_core`

contains the core definitions of the labelled transition system of the π-calculus and the definition of bisimulation-up-to. There are also some simple lemmas about ordinary bisimulation (*a.k.a.*bisimulation up to reflexivity).`pic_bisim`

contains the soundness proof of*bisimulation up to bisimilarity*.`pic_ctx`

contains a proof that par and nu contexts are substitutive.

Examples

`pic_bisim_examples`

contains some examples of the use of the up-to-bisimilarity technique to show the bisimilarity of processes that have only infinite bisimulations. Note: some of these proofs are parametric on an assumed structural congruence for replication.

Package

`pic.tar.gz`

, which packages up the above files together with a`Makefile`

to run the sources through Abella in the right order.

Last updated: