Sitemap

Pages

• About

• Publications

• Teaching

• Talks

• CV

Publications

• Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM (2026)

• Uniform interpolation with constructive diamond (2026)

• Intuitionistic Justification Logic, Semantically (2026)

• Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason (2026)

• Semantical Analysis of Intuitionistic Modal Logics between CK and IK (2025)

• Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents (2025)

• Completeness of First-Order Bi-Intuitionistic Logic (2025)

• Constructive algebraic completeness of first-order bi-intuitionistic logic (2025)

• Towards computing uniform interpolants for KM in Rocq (2025)

• Intuitionistic S4 as a logic of topological spaces (2024)

• Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL (2024)

• A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic (2024)

• A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised (2023)

• New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq (2023)

• Mechanised constructive reverse mathematics: soundness and completeness of bi-intuitionistic logic (2023)

• Non-compactness and converse well-foundedness (2023)

• Towards compact semantics for intuitionistic provability logic (2023)

• Direct elimination of additive-cuts in GL4ip: verified and extracted (2022)

• First-Order Bi-Intuitionistic Logics: From Shaky to Formally Verified Foundations (2022)

• Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq (2021)

• Bi-Intuitionistic Logics: A New Instance of an Old Problem (2020)

• A multi-labelled sequent calculus for Topo-Logic (2020)

• Bi-Intuitionistic Types via Alternating Contexts (2020)

• Internalisation of the deducibility relation: the role of deduction theorems and modal logic (2017)

• Logic, meaning and negative translation (2016)