| 2026 | CSL | A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light. | Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi |
| 2026 | IJCAR | Growing HOLMS: A Verified Automated Prover for Grzegorczyk Logic in HOL Light. | Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi |
| 2024 | ISoLA | Analysing Collective Adaptive Systems by Proving Theorems. | Cosimo Perini Brogi, Marco Maggesi |
| 2024 | ISoLA | Rigorous Analysis of Idealised Pathfinding Ants in Higher-Order Logic. | Marco Maggesi, Cosimo Perini Brogi |
| 2022 | FOSSACS | Variable binding and substitution for (nameless) dummies. | Andr Hirschowitz, Tom Hirschowitz, Ambroise Lafont, Marco Maggesi |
| 2021 | ITP | A Formal Proof of Modal Completeness for Provability Logic. | Marco Maggesi, Cosimo Perini Brogi |
| 2018 | CSL | High-Level Signatures and Initial Semantics. | Benedikt Ahrens, Andr Hirschowitz, Ambroise Lafont, Marco Maggesi |
| 2017 | ITP | Formalizing Basic Quaternionic Analysis. | Andrea Gabrielli, Marco Maggesi |
| 2007 | WoLLIC | Modules over Monads and Linearity. | Andr Hirschowitz, Marco Maggesi |