CCS in nominal logic (Q7361356)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry CCS
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | CCS in nominal logic |
AFP entry CCS |
Statements
29 May 2012
0 references
Jesper Bengtson
0 references
CCS in nominal logic (English)
0 references
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 .
0 references
