# Cosimo Perini Brogi

PhD in Mathematics and Applications

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

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

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.

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

## Varia

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