An operational semantics in Isabelle/HOL-CSP

DOI10.4230/LIPICS.ITP.2024.7MaRDI QIDQ6860030zbMATH OpenFDO

Authors Benoît Ballenghien, Burkhart Wolff

Publication date 10 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2024.7

zbMATH Keywords

computational modelsconcurrencyIsabelle/HOLprocess-algebrasemanticstheorem proving

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A Complete Axiomatic Semantics for the CSP Stable-Failures Model
• A Theory of Communicating Sequential Processes
• An Alternative Order for the Failures Model
• From algebra to operational semantics
• HOLCF = HOL + LCF
• scientific article; zbMATH DE number 3902016 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 2080001 (Why is no real title available?)
• scientific article; zbMATH DE number 3379785 (Why is no real title available?)
• Philosophers May Dine - Definitively!
• Theories of programming and formal methods. Essays dedicated to Jifeng He on the occasion of his 80th birthday
• Understanding concurrent systems

Cited in

(4)

• A theory of Proc-Omata -- and proof methods for process architectures
• Operational Semantics formally proven in HOL-CSP
• Parameterized Termination for Sequential Composition and Synchronization Product
• A Bridge between CSP Processes and Functional Automata

This page was built for publication: An operational semantics in Isabelle/HOL-CSP

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6860030)