Cosimo Perini Brogi

Contact details

Arthur Rackham, Advice from a Caterpillar, 1907
(Public domain) Name: Cosimo ∂
Surname: Perini Brogi
SySMA Unit
IMT 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 2022CY2J5S 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
• Toward dynamic epistemic verification of zero-knowledge protocols (joint work with Gabriele Costa), Proceedings of the 8th Italian Conference on Cyber Security (ITASEC 2024), Salerno, Italy, April 8-12, 2024, CEUR Workshop Proceedings Vol. 3731, Open AccessCEUR-WS.org

ORCID Account

DBLP Profile

Further research output

• Toward dynamic epistemic verification of zero-knowledge protocols, Second Secure Software from First Principles Workshop, IMT School for Advanced Studies Lucca (June 13-14, 2024), slides
• Machine translation, problem solving, and pattern recognition: A historical-phenomenological analysis, Friedrich-Alexander-Universität Erlangen-Nürnberg (May 8, 2024), slides
• Toward dynamic epistemic verification of zero-knowledge protocols, Italian Conference on Cybersecurity 2024, Salerno (April 8-11 2024), slides
• 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 (Sept. 18-29, 2023), slides
• GL within HOL Light, Lightning 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), slides
• 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, DOI.
• 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, DOI.
• Computerised reasoning. The "dark side" of AI, SISSA Masterclass @ IMT Lucca, Nov. 2023Slides for the lightning talk.

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) First HAL preprints [1], [2] with Marco Maggesi
• 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)
• Logico-philosophical foundations for neural network systems (joint work with Stefania Centrone)

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.

For several reasons, I cannot endorse the following platforms: LinkedIn, Fabebook and relatives, ResearchGate, Scopus and friends, academia.edu, X-Twitter, ChatGPT et similia .

         α
λ            β