Cosimo Perini Brogi

Contact details

Arthur Rackham, Advice from a Caterpillar, 1907
(Public domain) Name: Cosimo ∂
Surname: Perini Brogi
SySMA Unit
School for Advanced Studies Lucca
Office 10 in Refettorio Hall
Piazza San Francesco 19
55100 Lucca
Tuscany, Italy

Email: cosimo.perinibrogi@X.Y
[where X=imtlucca Y=it]

My GnuPG public RSA key has the following signature:

 pub  rsa4096 2023-04-29 
      B1A465DE7E9905D158D43E1841FE7C5A82355E72
 uid  Cosimo-PB (IMTK) 

Research interests

My scientific interests stay at the intersection of computer science, mathematics, and philosophy.

Currently, I am assistant professor (RTDa) in theoretical computer science, working within the NextGenerationEU project “Securing softWare frOm first PrincipleS” (SERICS-SWOPS), led by Gabriele Costa.

My primary conceptual toolbox is based on structural proof theory and non-classical logics.

Over the years, I have worked on (classical and intuitionistic) modal logics, sequent calculi, natural deduction systems, functional programming languages and type systems, computerised mathematics, formal software verification.

I am also interested in mathematics in its broader cultural context, including the links between mathematics, literature and music.

More info

My previous post-doc position at IMT Lucca was funded by the PRIN 2017FTXR7S Project IT-Matters, and I worked on formal methods for decentralised and self-organising systems under the supervision of Rocco De Nicola.

Before that, in 2022, 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 Non-classical Logics Full text in open access
• Supervisors: Sara Negri, Pino Rosolini
• Examiners: Slides for the Viva Martin Hyland (King's College, Cambridge), Eugenio Orlandelli (Alma Mater Bologna), and Daniele Porello (University of Genoa)

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.

Publications

• Curry-Howard-Lambek Correspondence for Intuitionistic Belief, Studia Logica Volume 109 Issue 3, June 2021, Open AccessDOI
• A formal proof of modal completeness for provability logic (joint work with Marco Maggesi), LIPIcs, Volume 193, ITP 2021, Open AccessDOI
• Mechanising Gödel-Löb provability logic in HOL Light (joint work with Marco Maggesi), Journal of Automated Reasoning 67:29, August 2023, Open AccessDOI

ORCID Account

DBLP Profile

Further research output

• Proof systems for interpretability logics, PACMAN Workshop, University of Verona (March 20, 2024)
• Theorem provers within theorem provers, International Summer School on Interactions of Proof Assistants and Mathematics, University of Regensburg (18-29 Sept. 2023), slides
• GL within HOL Light, Flash Talk at Proof and Computation Autumn School (Sept. 2023), slides
• Towards a proof analysis of processes, IT-Matters Final Workshop, IMT School for Advanced Studies Lucca, (July 12, 2023)
• Results and ideas on proof theory for interpretability logics, 4th International Workshop on Proof Theory and Applications (Nov. 12, 2022), abstract and slides
• A formal proof of modal completeness for provability logic, ITP 2021 Talk (June 30, 2021), slides
• 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 Curry-Howard Correspondence for Intuitionistic Belief, Poster Session at The Proof Society Summer School, Computational Foundry-Swansea 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 2016-17, manuscript

Outreach

• L'enigma del compleanno, Archimede 3/2020, December 2020A contribution on Dynamic Epistemic Logic for the Italian journal of mathematics for the lay audience.
• L'evoluzione della scienza umana?, Febr. 2021A post in the blog MaddMaths! on Computerised Mathematics for the lay audience (in Italian).
• Perché leggere i classici (delle dimostrazioni matematiche), Febr. 2021An informal hypertext on Proof Mining for the general audience (in Italian).
• La matematica delle dimostrazioni, Archimede 2/2022, October 2022A contribution on Proof Theory and Applications for the Italian journal of mathematics for the lay audience.

Work in progress

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.

• Knowledge flow in Ali Baba's cave, and more (joint work with Gabriele Costa)
• An ant's life (Experiments in certified bio-informatics)
• Universal Algebra in UniMath (joint work with Gianluca Amato, Matteo Calosci and Marco Maggesi) ArXiv preprint
• The Coq Knight: Homage to G. Perec (very experimental)
• Proof analysis for interpretability logics (joint work with Sara Negri and Nicola Olivetti)

Varia

I am a member of the EC-COST Action (CA20111) EuroProofNet, the IMT Extended MInD Group, the Association Computability in Europe, The Proof Society, the CLAI Lab for Computational Logic and Artificial Intelligence, the INdAM, GNSAGA Group.

         α
λ            β