Cosimo Perini Brogi
PhD in Mathematics and Applications

Name: Cosimo
SySMA Unit Email: cosimo.perinibrogi@X.Y [where X=imtlucca Y=it] ORCID: 0000000178835727 
Member of The Proof Society
Member of EuroProofNet
Member of INdAM, GNSAGA
My current project is focused on formal methods for decentralised and selforganising systems.
My primary conceptual toolbox is based on structural proof theory and nonclassical logics.
Over the years, I have worked with (classical and intuitionistic) modal logics, sequent calculi, natural deduction systems, functional programming languages and type systems, computerised mathematics, software verification.
I am also interested in mathematics in its broader cultural context, including the links between mathematics, literature and music.
My position is funded by the PRIN 2017FTXR7S Project ITMatters, and I work under the supervision of Rocco De Nicola.
Previously, I worked on mathematical modal logics and software verification at the University of Barcelona, supervised by Joost J. Joosten and supported by an "academic+industrial" grant.
On July 12, 2022, I successfully defended my PhD thesis at the Department of Mathematics of the University of Genoa
 Title: Investigations of Proof Theory and Automated Reasoning for Nonclassical Logics
 Supervisors: Sara Negri, Pino Rosolini
 Examiners: Martin Hyland (King's College, Cambridge), Eugenio Orlandelli (Alma Mater Bologna), and Daniele Porello (University of Genoa)
 Slides for the Viva
 Full text in open access
In 2018, I obtained a MA degree in Logic, Philosophy and History of Science from the University of Florence, with a dissertation on category theory in univalent type theory supervised by Marco Maggesi.
Previously, in 2015, I graduated in Philosophy from the same University with a thesis on Solovay's arithmetical completeness theorem supervised by Pierluigi Minari.
I have occasionally worked as a gardener and woodcutter.
 CurryHowardLambek Correspondence for Intuitionistic Belief, Studia Logica Volume 109 Issue 3, June 2021, DOI:10.1007/s11225021099523 (Open Access)
 A formal proof of modal completeness for provability logic (joint work with Marco Maggesi), LIPIcs, Volume 193, ITP 2021, DOI:10.4230/LIPIcs.ITP.2021.26 (Open Access)
 Universal Algebra in UniMath (joint work with Gianluca Amato and Marco Maggesi), arXiv preprint here
 L'enigma del compleanno, Archimede 3/2020 (a contribution on Dynamic Epistemic Logic for the Italian journal of mathematics for the large audience) Dec. 2020
 La matematica delle dimostrazioni, Archimede 2/2022 (a contribution on Pure and Applied Proof Theory for the Italian journal of mathematics for the large audience) October 2022
 Mechanising GödelLöb provability logic in HOL Light (joint work with Marco Maggesi), Journal of Automated Reasoning 67,29 August 2023 DOI: 10.1007/s1081702309677z (Open Access)
 Theorem provers within theorem provers, International Summer School on Interactions of Proof Assistants and Mathematics, University of Regensburg (1829 Sept. 2023), slides
 GL within HOL Light, Flash Talk at Proof and Computation Autumn School (Sept. 2023), slides
 Results and ideas on proof theory for interpretability logics, 4th International Workshop on Proof Theory and Applications (Nov. 12, 2022), abstract and slides
 Perché leggere i classici (delle dimostrazioni matematiche), An informal article on Proof Mining for the large audience, hypertext (in Italian)
 A formal proof of modal completeness for provability logic, ITP 2021 Talk (June 30, 2021), slides
 L'evoluzione della scienza umana?, A post in the blog MaddMaths! on Computerised Mathematics for the large audience (in Italian), Febr. 2021
 Analytic Proof Systems for Provability Logic, Logic Seminar, University of Genoa, Sept. 2020, slides
 Universal Algebra in UniMath, HoTT/UF 2020 Talk (July 7, 2020), video
 A CurryHoward Correspondence for Intuitionistic Belief, Poster Session at The Proof Society Summer School, Computational FoundrySwansea University, Sept. 2019
 An introduction to Normal Modal Logics, Logic Seminar, University of Genoa, Summer 2019
 Categorical Semantics for Intuitionistic Belief, Logic and Philosophy of Science Seminar, University of Florence, May 2019
 Kleisli Triples in Homotopy Type Theory, MA Dissertation, Code in UniMath Repository, Dec. 2017
 An Overview of Simple Type Theory, Final Year Report, Graduate Student Seminar 201617, manuscript
Disclaimer : Some of the titles below are intentionally preposterous, except for the ones of those papers that are currently under review or ready for submission.
 An ant's life (Experiments in bioinformatics)
 Universal Algebra in UniMath (joint work with Gianluca Amato and Marco Maggesi), arXiv preprint here
 The Coq Knight: Homage to G. Perec (very experimental)
My GnuPG public RSA key for the "IMT" address has the following signature:
pub rsa4096 20230429 B1A465DE7E9905D158D43E1841FE7C5A82355E72 uid CosimoPB (IMTK)sub rsa4096 20230429
“Se si escludono istanti prodigiosi e singoli che il destino ci può donare, l'amare il proprio lavoro (che purtroppo è privilegio di pochi) costituisce la migliore approssimazione concreta alla felicità sulla terra: ma questa è una verità che non molti conoscono. ”
— Primo Levi, La chiave a stella, 1978