Marco Maggesi

38 papers B 7C 1Journal 23Unranked 7
YearRankTypeTitle / Venue / Authors
2026 B conf
A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light.
CSL
Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi
2025 — conf
A Modular Proof of Semantic Completeness for Normal Systems beyond the Modal Cube, Formalised in HOLMS.
ICTCS
Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi
2025 J jnl
Bridging higher-order logic and efficient computations for a rigorous analysis of idealised pathfinding ants.
Int. J. Softw. Tools Technol. Transf.
Cosimo Perini Brogi, Marco Maggesi
2025 — conf
Displayed Universal Algebra in UniMath: Basic Definitions and Results.
ICTCS
Gianluca Amato, Matteo Calosci, Marco Maggesi, Cosimo Perini Brogi
2025 — conf
Recurrent Neural Networks for Guiding Proof Search in Propositional Logic.
ICTCS
Gianluca Amato, Nicola Balestra, Marco Maggesi, Maurizio Parton
2024 — conf
Analysing Collective Adaptive Systems by Proving Theorems.
ISoLA (1)
Cosimo Perini Brogi, Marco Maggesi
2024 — conf
Growing HOLMS, a HOL Light Library for Modal Systems.
OVERLAY
Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini
2024 — conf
Rigorous Analysis of Idealised Pathfinding Ants in Higher-Order Logic.
ISoLA (2)
Marco Maggesi, Cosimo Perini Brogi
2024 J jnl
Universal algebra in UniMath.
Math. Struct. Comput. Sci.
Gianluca Amato, Matteo Calosci, Marco Maggesi, Cosimo Perini Brogi
2024 J jnl
Variable binding and substitution for (nameless) dummies.
Log. Methods Comput. Sci.
André Hirschowitz, Tom Hirschowitz, Ambroise Lafont, Marco Maggesi
2023 J jnl
Mechanising Gödel-Löb Provability Logic in HOL Light.
J. Autom. Reason.
Marco Maggesi, Cosimo Perini Brogi
2022 J jnl
A theorem prover and countermodel constructor for provability logic in HOL Light.
CoRR
Marco Maggesi, Cosimo Perini Brogi
2022 B conf
Variable binding and substitution for (nameless) dummies.
FoSSaCS
André Hirschowitz, Tom Hirschowitz, Ambroise Lafont, Marco Maggesi
2022 J jnl
Variable binding and substitution for (nameless) dummies.
CoRR
André Hirschowitz, Tom Hirschowitz, Ambroise Lafont, Marco Maggesi
2021 B conf
A Formal Proof of Modal Completeness for Provability Logic.
ITP
Marco Maggesi, Cosimo Perini Brogi
2021 J jnl
A formal proof of modal completeness for provability logic.
CoRR
Marco Maggesi, Cosimo Perini Brogi
2021 J jnl
Bicategories in univalent foundations.
Math. Struct. Comput. Sci.
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide
2021 J jnl
Presentable signatures and initial semantics.
Log. Methods Comput. Sci.
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2021 J jnl
Universal Algebra in UniMath.
CoRR
Gianluca Amato, Marco Maggesi, Cosimo Perini Brogi
2020 J jnl
Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System.
CoRR
Marco Maggesi, Massimo Nocentini
2020 J jnl
Reduction monads and their signatures.
Proc. ACM Program. Lang.
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2020 J jnl
Universal Algebra in UniMath.
CoRR
Gianluca Amato, Marco Maggesi, Maurizio Parton, Cosimo Perini Brogi
2019 B conf
Bicategories in Univalent Foundations.
FSCD
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
2019 J jnl
Bicategories in Univalent Foundations.
CoRR
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
2019 B conf
Modular Specification of Monads Through Higher-Order Presentations.
FSCD
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2019 J jnl
Modular specification of monads through higher-order presentations.
CoRR
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2019 J jnl
Reduction Monads and Their Signatures.
CoRR
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2018 J jnl
A Formalization of Metric Spaces in HOL Light.
J. Autom. Reason.
Marco Maggesi
2018 B conf
High-Level Signatures and Initial Semantics.
CSL
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2018 J jnl
High-level signatures and initial semantics.
CoRR
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2017 B conf
Formalizing Basic Quaternionic Analysis.
ITP
Andrea Gabrielli, Marco Maggesi
2012 — conf
Initial Semantics for Strengthened Signatures
FICS
André Hirschowitz, Marco Maggesi
2012 J jnl
Nested Abstract Syntax in Coq.
J. Autom. Reason.
André Hirschowitz, Marco Maggesi
2011 J jnl
A Certified Proof of the Cartan Fixed Point Theorems.
J. Autom. Reason.
Gianni Ciolli, Graziano Gentili, Marco Maggesi
2010 J jnl
Modules over monads and initial semantics.
Inf. Comput.
André Hirschowitz, Marco Maggesi
2007 C conf
Modules over Monads and Linearity.
WoLLIC
André Hirschowitz, Marco Maggesi
2007 J jnl
The algebraicity of the lambda-calculus
CoRR
André Hirschowitz, Marco Maggesi
2006 J jnl
Modules over Monads and Linearity
CoRR
André Hirschowitz, Marco Maggesi