Talks

Invited Talks

• Artificial Mathematics
  12 December 2024, Urbino (online)

• Growing HOLMS, a HOL Light Library for Modal Systems (slides, webpage)
  OVERLAY 2024 – 6th International Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis
  28 and 29 November, Bolzano (Italy)

• Building proofs and countermodels in HOL Light of the provability logic GL (slides, webpage, video)
  Trimester Program “Prospects of Formal Mathematics”,
  August 8, 2024, Hausdorff Institut für Mathematik, Bonn, Germany

• Matematica formale per la metateoria e la simulazione dei sistemi complessi (slides)
  May 22, 2024, Simposio su Sistema, Complessità e Natura, Florence, Italy

• The HOL Light library of formalized mathematics  (slides)
  EuroProofNet Workshop on the development, maintenance, refactoring and search of large libraries of proofs
  September 23, 2022,  Tbilisi, Georgia

• (Categories and) Bicategories in Univalent Foundations (slides)
  ItaCa 3rd ItaCa Workshop
  December 22, 2022, Pisa, Italy

• Explaining Basic Quaternionic Analysis to the Computer (slides)
  Incontro Nazionale di Analisi Ipercomplessa
  December 19, 2022, Florence, Italy

• Bicategories in Univalent Foundations (slides)
  Cats60 – Celebrating Carlos Simpson’s 60th birthday
  June 24, 2022, Toulouse, France

• Bicategories in Univalent Foundations (slides)
  Department of Mathematics "Tullio Levi Civita"
  May 31, 2022,  University of Padua, Padua, Italy

• Una introduzione visiva al Machine Learning e al Deep Learning (slides)
  Workshop on "Intelligenza Artificiale e Humanities: una macchina senza qualità",
  ISPF - Istituto Scientifico del Pensiero Filosofico e Scientifico Moderno - CNR,
  May 3, 2022, Naples, Italy

• Matematica artificiale (slides)
  PhD in Mathematics, Computer Science and Statistics
  University of Florence
  Genuary 19, 2022, Florence, Italy

• Artificial mathematics
  Giornata dei borsisti INdAM– Cofund
  INdAM – Istituto Nazionale di Alta Matematica
  October 27, 2021, Rome (online)

• Studying the mobility of people and the spread of ideas through machine learning (slides)
  Workshop on “Models for people in motion in the Mediterranean basin” Rome (online), 2021-04-23

• Universal Algebra in UniMath (slides, demo)
  Department of Software Science of Tallinn University of Technology
  February 2021, online, Tallinn (Estonia) 

• Theorems as Data (slides)
  First Workshop of the Florence Center for Data Science
  June 10, 2019, Florence, Italy

• Formalizing (hyper)complex analysis (slides)
  Team Marelle, INRIA, Sophia-Antipolis
  May 14, 2019, Sophia-Antipolis, France

• Formal Methods for the Working Mathematician (slides)
  PhD in Mathematics, University of Bologne
  January 24, 2019, Bologne, Italy

• A formalization of metric spaces in HOL Light (slides)
  GnCS 2017 - Geometry and Computer Science
  Dipartimento di Economia dell'Università di Chieti-Pescara
  February 8–10, 2017, Pescara, Italia

• Some elementary remarks on lci algebraic cycles
  September 2016, Chinese Academy of Studies (CAS), Beijin, China

Public Outreach Talks

• Strumenti didattico–visivi per l'introduzione dell’AI (slides)
  December 14, 2023, Chi ha paura dell’AI?
  Organizzato da DirigentiScuola Toscana.  Florence, Italy.

• Intelligenza Percepita
  Incontro su "Etica e robotica. Verso la società dell’intelligenza artificiale"
  CRS - Centro per la Riforma dello Stato
  February 2, 2023.  Florence, Italy.

• From Algebraic Geometry to Proof Assistants (slides, paper)
  “How to solve your next math problem by computer. Three stories on proof-assistants”,
  “A collective talk for all undergraduate/graduate students in mathematics and computer science”,
  June 7, 2022, Dipartimento di Matematica dell’Università di Padova, Padua, Italy.

• Bitcoin, criptovalute e contratti intelligenti (slides, in Italian)
  Ciclo di lezioni: "Mutamenti del pensiero matemtematico"
  June 13,  2019, Accademia la Colombaria, Florence, Italy

• Metodi formali per la pratica matematica
  Ciclo di conferenze: "Teoria della dimostrazione: Tra matematica e filosofia"
  Associazione Studentesca Matematica Pavese, Collegio Ghislieri
  April 15, 2019, Pavia, Italy

• Metodi formali in matematica (slides, in Italian)
  Ciclo di lezioni: "Mutamenti del pensiero matemtematico"
  May 30, 2019, Accademia la Colombaria, Florence, Italy

• Teoria della computabilità in HOL (slides, in Italian)
  May 2017, Seminario di Logica e Filosofia della Scienza

Conference and Workshop Contributions

• Proof Assistants in Higher Education
  Innovative STEM teaching in Higher Education: from theory to action, 2025-05-30 Florence, Italy

• Building proofs and countermodels in HOL Light of the provability logic GL (slides)
  Applied Proof Theory (APT22)
  August 29 — September 02, 2022, Pescara, Italy

• Bicategories in Univalent Foundations (slides)
  Algebra and Algorithms
  February 2020, Djerba, Tunisia

• Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System  (webpage, paper)
  miniKanren 2020 – miniKanren and Relational Programming Workshop
  Part of ICFP 2020 – The 25th ACM SIGPLAN International Conference on Functional Programming
  February 25, 2021, Online.

• Universal Algebra in UniMath (abstract,  video, webpage)
  Gianluca Amato, Marco Maggesi, Maurizio Parton and Cosimo Perini Brogi
  Presented by Cosimo Perini Brogi
  Workshop on Homotopy Type Theory/Univalent Foundations
  Co-located with FSCD 2020
  July 05–07, 2020, online.

• Private types in Higher Order Logic Programming  (video, abstract)
  Marco Maggesi and Enrico Tassi
  Presented by Enrico Tassi
  TEASE-LP 2020 - Workshop on Trends, Extensions, Applications and Semantics of Logic Programming”
  May 28-29, 2020, online.

• Reduction Monads and Their Signatures (slides and video)
  POPL 2020 - 47th ACM SIGPLAN Symposium on Principles of Programming Languages
  January  19–25, 2020, New Orleans, USA

• Formalizing Basic Quaternionic Analysis (slides)
  8th International Conference on Interactive Theorem Proving, ITP 2017
  September 26–29, 2017, Brasília, Brazil

• De Bruijn Monads (slides)
  April 2017, FPFM 2017 - Workshop on Foundations for the practical formalization of mathematics