### Abstract

We formalise a large portion of CCS as described in Milner's book 'Communication and Concurrency' using the nominal datatype package in Isabelle. Our results include many of the standard theorems of bisimulation equivalence and congruence, for both weak and strong versions. One main goal of this formalisation is to keep the machine-checked proofs as close to their pen-and-paper counterpart as possible.

This entry is described in detail in Bengtson's thesis.

### License

BSD License

### Topics

- Computer science/Concurrency/Process calculi

### Session CCS

- Agent
- Tau_Chain
- Weak_Cong_Semantics
- Weak_Semantics
- Strong_Sim
- Weak_Sim
- Weak_Cong_Sim
- Strong_Sim_SC
- Strong_Bisim
- Strong_Sim_Pres
- Strong_Bisim_Pres
- Struct_Cong
- Strong_Bisim_SC
- Weak_Bisim
- Weak_Cong
- Weak_Sim_Pres
- Weak_Bisim_Pres
- Weak_Cong_Sim_Pres
- Weak_Cong_Pres

## Cite

×

CCS-AFP

    @article{CCS-AFP,
      author  = {Jesper Bengtson},
      title   = {CCS in nominal logic},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/CCS.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- Jun 14, 2012 : Isabelle2012