Cosimo Perini Brogi

PhD in Mathematics and Applications

Contact details

CatArthur 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 
 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

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.


  • 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

  • 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


  • 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.

  • 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)


I am a member of The Proof Society, the EC-COST Action (CA20111) EuroProofNet, the Association Computability in Europe, the INdAM, GNSAGA Group.


About this site

This website is based on a slightly modified version of Tufte CSS.

Last update: January 2024

“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