| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
CCS in nominal logic
| Title: | CCS in nominal logic |
| Author: | Jesper Bengtson |
| Submission date: | 2012-05-29 |
| 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. |
| BibTeX: |
@article{CCS-AFP,
author = {Jesper Bengtson},
title = {CCS in nominal logic},
journal = {Archive of Formal Proofs},
month = may,
year = 2012,
note = {\url{http://isa-afp.org/entries/CCS.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [skipped] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|