Benoît Ballenghien

Arch. Formal Proofs, 2026

Parameterized Termination for Sequential Composition and Synchronization Product.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2026

2025

HOL-CSP: A Comprehensive Process Theory for Semantics and Proc-Omata Reasoning. (HOL-CSP: Une théorie intégrée de processus pour raisonner sur les sémantiques et les Proc-Omata).

[BibT_eX]

[DOI]

PhD thesis, 2025

A Proof of Hilbert Basis Theorem and an Extension to Formal Power Series.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2025

CSP Semantics over Restriction Spaces.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2025

Ultrametric Structure for Restriction Spaces.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2025

Examples of Restriction Spaces.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2025

Restriction Spaces: a Fixed-Point Theory.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2025

Definition and Elementary Properties of Ultrametric Spaces.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2025

Sophie Germain's Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2025

2024

Event-B as DSL in Isabelle and HOL Experiences from a Prototype.

[BibT_eX]

[DOI]

Proceedings of the Rigorous State-Based Methods - 10th International Conference, 2024

An Operational Semantics in Isabelle/HOL-CSP.

[BibT_eX]

[DOI]

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

A Theory of Proc-Omata - and Proof Methods for Process Architectures.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2024, 2024

2023

Operational Semantics formally proven in HOL-CSP.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2023

HOL-CSPM - Architectural operators for HOL-CSP.

[BibT_eX]

[DOI]

Safouan Taha