Pietro Sabelli

sabelli@flu.cas.cz | GitHub Profile | CV

I am currently a postdoc at the Department of Logic of the Institute of Philosophy of the Czech Academy of Sciences working with Ansten Klev.

My research focuses on dependent type theories as foundations of mathematics, investigating both their syntax – explored with the help of proof-assistants such as Agda – and their semantics – primarily through the categorical notions of doctrines and fibrations. In particular, I am interested in the Minimalist Foundation as a common core for the plurality of foundational systems for mathematics.

In 2024, I defended my PhD thesis in Mathematics Around the Minimalist Foundation: (Co)Induction and Equiconsistency under the supervision of Maria Emilia Maietti and Samuele Maschio.

Publications

• Equiconsistency of the Minimalist Foundation with its classical version. With M. E. Maietti. Annals of Pure and Applied Logic, Volume 176, Issue 2. 2025
• A topological reading of coinductive predicates in Dependent Type Theory. Submitted. 2024. (Agda code)
• A topological counterpart of well-founded trees in dependent type theory. With M. E. Maietti. Electronic Notes in Theoretical Informatics and Computer Science, Volume 3. Proceedings of MFPS XXXIX. 2022. (Agda code)
• On the Compatibility Between the Minimalist Foundation and Constructive Set Theory. With S. Maschio. Revolutions and Revelations in Computability. CiE 2022. Lecture Notes in Computer Science, vol 13359. Springer, Cham. 2021

Selected Talks

• Peculiarities of the Minimalist Foundation for Formal Mathematics
  With M.E. Maietti. Hausdorff Research Institute for Mathematics. June 2024
  (Slides)
• Inductive and Coinductive predicates in the Minimalist Foundation
  University of Kyoto. September 2023
  (Abstract) (Slides)