Modules over Monads and Linearity. - André Hirschowitz; Marco Maggesi (WoLLIC, 2007)

The algebraicity of the lambda-calculus - André Hirschowitz; Marco Maggesi (CoRR, 2007)

Modules over monads and initial semantics. - André Hirschowitz; Marco Maggesi (Inf. Comput., 2010)

A Certified Proof of the Cartan Fixed Point Theorems. - Gianni Ciolli; Graziano Gentili; Marco Maggesi (J. Autom. Reason., 2011)

Initial Semantics for Strengthened Signatures - André Hirschowitz; Marco Maggesi (FICS, 2012)

Nested Abstract Syntax in Coq. - André Hirschowitz; Marco Maggesi (J. Autom. Reason., 2012)

Formalizing Basic Quaternionic Analysis. - Andrea Gabrielli; Marco Maggesi (ITP, 2017)

High-Level Signatures and Initial Semantics. - Benedikt Ahrens; André Hirschowitz; Ambroise Lafont; Marco Maggesi (CSL, 2018)

A Formalization of Metric Spaces in HOL Light. - Marco Maggesi (J. Autom. Reason., 2018)

Bicategories in Univalent Foundations. - Benedikt Ahrens; Dan Frumin; Marco Maggesi; Niels van der Weide (FSCD, 2019)

Modular Specification of Monads Through Higher-Order Presentations. - Benedikt Ahrens; André Hirschowitz; Ambroise Lafont; Marco Maggesi (FSCD, 2019)

Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System. - Marco Maggesi; Massimo Nocentini (CoRR, 2020)

Universal Algebra in UniMath. - Gianluca Amato; Marco Maggesi; Maurizio Parton; Cosimo Perini Brogi (CoRR, 2020)

Reduction monads and their signatures. - Benedikt Ahrens; André Hirschowitz; Ambroise Lafont; Marco Maggesi (Proc. ACM Program. Lang., 2020)

A Formal Proof of Modal Completeness for Provability Logic. - Marco Maggesi; Cosimo Perini Brogi (ITP, 2021)

Universal Algebra in UniMath. - Gianluca Amato; Marco Maggesi; Cosimo Perini Brogi (CoRR, 2021)

Presentable signatures and initial semantics. - Benedikt Ahrens; André Hirschowitz; Ambroise Lafont; Marco Maggesi (Log. Methods Comput. Sci., 2021)

Bicategories in univalent foundations. - Benedikt Ahrens; Dan Frumin; Marco Maggesi; Niccolò Veltri; Niels van der Weide (Math. Struct. Comput. Sci., 2021)

A theorem prover and countermodel constructor for provability logic in HOL Light. - Marco Maggesi; Cosimo Perini Brogi (CoRR, 2022)

Mechanising Gödel-Löb Provability Logic in HOL Light. - Marco Maggesi; Cosimo Perini Brogi (J. Autom. Reason., 2023)

Analysing Collective Adaptive Systems by Proving Theorems. - Cosimo Perini Brogi; Marco Maggesi (ISoLA (1), 2024)

Rigorous Analysis of Idealised Pathfinding Ants in Higher-Order Logic. - Marco Maggesi; Cosimo Perini Brogi (ISoLA (2), 2024)

Growing HOLMS, a HOL Light Library for Modal Systems. - Antonella Bilotta; Marco Maggesi; Cosimo Perini Brogi; Leonardo Quartini (OVERLAY, 2024)

Variable binding and substitution for (nameless) dummies. - André Hirschowitz; Tom Hirschowitz; Ambroise Lafont; Marco Maggesi (Log. Methods Comput. Sci., 2024)

Universal algebra in UniMath. - Gianluca Amato; Matteo Calosci; Marco Maggesi; Cosimo Perini Brogi (Math. Struct. Comput. Sci., 2024)