# People

### About me

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

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.

Between 2022 and 2023, I worked on modal logics for meta-mathematics and certified programming at the University of Barcelona, supported by an "academic+industrial" grant from the Catalan Foundation for Research and Innovation.

I successfully defended my PhD thesis at the Department of Mathematics of the University of Genoa in July 2022.

### Research Activities

My specialisation centres on mathematical logic, with research spanning the domains of computer science, mathematics, and philosophy.

My main focus areas include:

Proof theory and interactive theorem proving

Non-classical logics

Type theory and computerised reasoning

I have worked on (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 the interplay between mathematics, literature, and music.

### Selected Publications

M. Maggesi, C. Perini Brogi. Mechanising Gödel–Löb Provability Logic in HOL Light. Journal of Automated Reasoning 67, 29 (2023). doi: 10.1007/s10817-023-09677-z

C. Perini Brogi. La matematica delle dimostrazioni in Archimede : 2, 2022, pp. 77-86, Le Monnier Firenze (2022). doi: 10.1400/288957.

M. Maggesi, C. Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021). doi: 10.4230/LIPIcs.ITP.2021.26.

See my DBLP page for a full list of publications. Additional research output of mine is collected in my personal webpage.