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.