Email Gateway (Aug 22 2022 at 19:30): Email Gateway (Aug 22 2022 at 19:30):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce a new and quite large development by Safouan, Lina Ye and Burkhart Wolff:
"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.”
It is online at https://www.isa-afp.org/entries/HOL-CSP.html
And I’ve taken the liberty of introducing a new topic: Computer Science/Semantics
Larry
Last updated: Nov 21 2024 at 12:39 UTC