Email Gateway (Dec 09 2023 at 18:55): Email Gateway (Dec 09 2023 at 18:55):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m happy to announce a new AFP entry.
Enjoy,
René
HOL-CSPM - Architectural operators for HOL-CSP
by Benoît Ballenghien, Safouan Taha and Burkhart Wolff
Recently, a modern version of Roscoes and Brookes Failure-Divergence Semantics
for CSP has been formalized in Isabelle: HOL-CSP. The session HOL-CSP introduces
among other things some binary operators on processes that we will here
generalize in a fully-abstract way. On these "architectural operators", we will
prove the properties of refinement, the rules of continuity and the laws of
interaction so that they can be easily used. Finally, we will give examples of
their usefulness when trying to model complex systems.
https://www.isa-afp.org/entries/HOL-CSPM.html
Last updated: Jan 04 2025 at 20:18 UTC