Abstract
We use the Restriction_Spaces library as a semantic foundation for the process algebra framework HOL-CSP, offering a complementary backend to the existing HOLCF infrastructure. The type of processes is instantiated as a restriction space, and we prove that it is complete in this setting. This enables the construction of fixed points for recursive process definitions without having to rely exclusively on a pointed complete partial order. Notably, some operators are constructive without being Scott-continuous, and vice versa, illustrating the genuine complementarity between the two approaches. We also show that key CSP operators are either constructive or non-destructive, and verify the admissibility of several predicates, thereby supporting automated reasoning over recursive specifications.
License
Topics
Session HOL-CSP_RS
- Process_Restriction_Space
- Prefixes_Constructive
- Choices_Non_Destructive
- Renaming_Non_Destructive
- Sequential_Composition_Non_Destructive
- Synchronization_Product_Non_Destructive
- Throw_Non_Destructive
- Interrupt_Non_Destructive
- After_Operator_Non_Too_Destructive
- Hiding_Destructive
- CSP_Restriction_Adm
- HOL-CSP_RS