HOL-CSPM - Architectural operators for HOL-CSP. - Benoît Ballenghien; Safouan Taha; Burkhart Wolff (Arch. Formal Proofs, 2023)

Operational Semantics formally proven in HOL-CSP. - Benoît Ballenghien; Burkhart Wolff (Arch. Formal Proofs, 2023)

A Theory of Proc-Omata - and Proof Methods for Process Architectures. - Benoît Ballenghien; Burkhart Wolff (ICTAC, 2024)

An Operational Semantics in Isabelle/HOL-CSP. - Benoît Ballenghien; Burkhart Wolff (ITP, 2024)

Event-B as DSL in Isabelle and HOL Experiences from a Prototype. - Benoît Ballenghien; Burkhart Wolff (ABZ, 2024)

Sophie Germain's Theorem. - Benoît Ballenghien (Arch. Formal Proofs, 2025)

Definition and Elementary Properties of Ultrametric Spaces. - Benoît Ballenghien; Benjamin Puyobro; Burkhart Wolff (Arch. Formal Proofs, 2025)

Restriction Spaces: a Fixed-Point Theory. - Benoît Ballenghien; Benjamin Puyobro; Burkhart Wolff (Arch. Formal Proofs, 2025)

Examples of Restriction Spaces. - Benoît Ballenghien; Benjamin Puyobro; Burkhart Wolff (Arch. Formal Proofs, 2025)

Ultrametric Structure for Restriction Spaces. - Benoît Ballenghien; Benjamin Puyobro; Burkhart Wolff (Arch. Formal Proofs, 2025)

CSP Semantics over Restriction Spaces. - Benoît Ballenghien; Burkhart Wolff (Arch. Formal Proofs, 2025)

A Proof of Hilbert Basis Theorem and an Extension to Formal Power Series. - Benjamin Puyobro; Benoît Ballenghien; Burkhart Wolff (Arch. Formal Proofs, 2025)