Embedded Files
As an integral part of my research, I dedicate a significant amount of time to developing code for computer-based formalizations of mathematics. This includes creating and refining tactics and extensions for theorem provers.
My work aims to advance the automation and precision of mathematical formalizations, contribute to research on the foundations of mathematics, and enhance the usability of formalization tools.
This page showcases some of my most significant contributions.
Social coding
Social coding
Selected projects and repositories
Selected projects and repositories
Listed approximately in reverse chronological order.
HOLMS: HOL Light Library for Modal Systems
Authors: Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini
https://holms-lib.github.io/HOL-Ants: Pathfinding ants formalised in the HOL Light theorem prover
Authors: Marco Maggesi, Cosimo Perini Brogi
(Github repository)Universal Algebra in UniMath
Authors: Gianluca Amato, Matteo Calosci, Marco Maggesi, Cosimo Perini Brogi
(Github repository)Modal completeness for the provability logic GL in HOL Light
(Folder in the HOL Light distribution, Permalink on SH)Initial algebra semantics for de Bruijn monads in HOL Light
Authors: Marco Maggesi
(Github repository, Permalink on SH, Permalink on Zenodo, DOI: 10.5281/zenodo.7053686)Bicategories in UniMath
Authors: Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weiden
(Folder on Github)Formalization of Quaternionic Calculus in HOL Light
Authors: Andrea Gabrielli, Marco Maggesi
(Bitbucket repository, Folder in the HOL Light distribution, Permalink on SH)Formalisation of Metric Spaces in HOL Light
Marco Maggesi
(Bitbucket repository, Pemalink on SH)Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System
Marco Maggesi, Massimo Nocentini
(Github repository)
Other projects and repositories of code that I contributed to
Other projects and repositories of code that I contributed to
Page updated
Report abuse