Email Gateway (Feb 03 2026 at 18:31): Email Gateway (Feb 03 2026 at 18:31):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Two new entries further extend the already substantial HOL-CSP collection in the AFP: one allows terminating processes to return values; another extends processes with a layer of automata. Warning: concurrency inside!
Parameterized Termination for Sequential Composition and Synchronization Product
by Benoît Ballenghien
Recently, parameterized termination has been introduced in HOL-CSP, allowing the termination event tick to carry a result value, in a way analogous to the return of a state monad. This conservative extension of the CSP theory required the generalization of several denotational definitions and the adaptation of numerous proofs. Since Isabelle2025, this work has been completed for the HOL-CSP, HOL-CSPM, and HOL-CSP_OpSem sessions. However, for two operators—namely sequential composition and the synchronization product—the most direct generalizations turn out to be conceptually unsatisfactory, in particular with respect to their interaction with SKIP. To address this issue, we introduce in this entry generalized versions of these operators that fully exploit the expressive power of parameterized termination; in particular, the resulting notion of sequential composition satisfies the monad laws. Building on these definitions, we establish a range of algebraic and operational laws, as well as fundamental properties such as continuity and non-destructiveness.
https://www.isa-afp.org/entries/HOL-CSP_PTick.html
A Bridge between CSP Processes and Functional Automata
by Benoît Ballenghien and Burkhart Wolff
This entry develops the Proc-Omata framework on top of HOL-CSP and its extensions. Proc-Omata are defined from functional automata and come in four variants: deterministic, terminating deterministic, non-deterministic, and terminating non-deterministic. This subclass of processes combines the expressiveness of CSP with automata-like structure (reachability, enableness), making it particularly amenable to invariant-based reasoning. We lift sequential composition and synchronization product to the automata level through combination functions and prove compactification theorems that enable reasoning over large process architectures. An essential ingredient is the use of restriction spaces, which guarantees well-defined fixed points even in the non-deterministic setting. Finally, we illustrate the applicability of the framework with the Dining Philosophers, where compactification yields proofs that scale to an arbitrary finite but unbounded number of participants in this parameterized process architecture.
https://www.isa-afp.org/entries/HOL-CSP_Proc-Omata.html
Enjoy!
Last updated: Feb 22 2026 at 05:16 UTC