### Abstract

This is a complete formalization of the work of Hoare and Roscoe on the denotational semantics of the Failure/Divergence Model of CSP. It follows essentially the presentation of CSP in Roscoe’s Book ”Theory and Practice of Concurrency” [8] and the semantic details in a joint Paper of Roscoe and Brooks ”An improved failures model for communicating processes". The present work is based on a prior formalization attempt, called HOL-CSP 1.0, done in 1997 by H. Tej and B. Wolff with the Isabelle proof technology available at that time. This work revealed minor, but omnipresent foundational errors in key concepts like the process invariant. The present version HOL-CSP profits from substantially improved libraries (notably HOLCF), improved automated proof techniques, and structured proof techniques in Isar and is substantially shorter but more complete.

### License

BSD License

### Topics

- Computer science/Concurrency/Process calculi
- Computer science/Semantics and reasoning

### Session HOL-CSP

- Introduction
- Process
- Bot
- Skip
- Stop
- Det
- Ndet
- Seq
- Hiding
- Sync
- Mprefix
- Mndetprefix
- CSP_Laws
- Process_Order
- CSP
- Assertions
- Conclusion
- CopyBuffer
- Induction_ext

### Used by

- HOL-CSPM - Architectural operators for HOL-CSP
- The HOL-CSP Refinement Toolkit

## Cite

×

HOL-CSP-AFP

    @article{HOL-CSP-AFP,
      author  = {Safouan Taha and Lina Ye and Burkhart Wolff},
      title   = {HOL-CSP Version 2.0},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/HOL-CSP.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
- Apr 29, 2019 : Isabelle2018