My main research interests lies in the area of homotopy type theory and semantics of dependent type theory. I am particularly interested in axiomatic (also know in the literature as weak, objective, propositional) type theory, where computation rules are all explicit. I study such formal systems via categorical semantics methods, in order to deduce properties like property-likeness, completeness, coherence, relative consistency, and conservativity.

I have also been working on the notions of hyperdoctrines and Grothendieck fibrations to approach the study of fragments of first-order logic, focusing on quantifier completions, the dialectica construction, and canonicity properties.

Lately, I have also been working on topics connected to temporal logics and circular reasoning.

Click here for a curriculum vitae and here for a research statement.

Ongoing research.

• Dialectica type theories. Together with Valeria de Paiva, Davide Trotta, and Jonathan Weinberger.
• Semantics of Spatio-temporal logic. Together with Davide Castelnovo and Marino Miculan.
• Constructive set theories within dependent type theory. Together with Emanuele Frittaion.
• Type constructors as algebras.
• Torsion theories and dependent types. Together with Federico Campanini.
• Coherence for path categories. Together with Daniël Otten and Benno van den Berg. YouTube presentation here.

Publications and preprints

• [Preprint] Higher dimensional semantics of axiomatic dependent type theory. [2507.07208]. January 2025.
• [Preprint] A biequivalence of path categories and axiomatic Martin Löf type theories. [2503.15431]. October 2024. Together with Daniël Otten.
• [Preprint] Towards propositional dependent sums in intensional and propositional dependent type theory. January 2024.
• [Preprint] The Gödel fibration (extended version). [2104.14021v1]. April 2021. Together with Davide Trotta and Valeria de Paiva.
• [Preprint] Quantifier completions, choice principles and applications. [2010.09111v3]. Submitted. October 2020. Together with Davide Trotta.

• [Journal paper] Relating homotopy equivalences to conservativity in dependendent type theories with propositional computation. [2303.05623v2]. Accepted for Logical Methods in Computer Science. June 2025.
• [Journal paper] Dialectica principles via Gödel doctrines. [2205.07093v1]. Theoretical Computer Science. February 2023. Together with Davide Trotta and Valeria de Paiva.
• [Journal paper] Dialectica logical principles: not only rules. Journal of Logic and Computation. December 2022. Together with Davide Trotta and Valeria de Paiva.

• [Refereed conference paper] Dialectica logical principles. [2109.08064v1]. Logical Foundations of Computer Science 2022. December 2021. Together with Davide Trotta and Valeria de Paiva.
• [Refereed conference paper] The Gödel fibration. Mathematical Foundations of Computer Science 2021. August 2021. Together with Davide Trotta and Valeria de Paiva.

• [PhD thesis] On the syntax and the semantics of propositional dependent type theories. Click here. July 2024.

Selected talks in conferences, workshops, seminars

• Higher dimensional semantics of propositional theories of dependent types. XVIII Incontro di Logica AILA. Udine, September 2024.
• Towards the coherence of the semantics of propositional identities. Nottingham Functional Programming Lunch. Nottingham, Februrary 2024.
• Coherence in the semantics of dependent types. Leeds Postgraduate Logic Seminar. Leeds, June 2023.
• Coherence for Extensional, Intensional and Propositional Identities. Category Theory Lunch. Leeds & Manchester, June 2023.
• What is a dependent type theory? Leeds Maths PGR Conference 2023. Leeds, June 2023.
• Strictifying Path Categories. Workshop on Doctrines & Fibrations. YouTube Recording. Slides. Padua, June 2023.
• Propositional dependent type theories: a conservativity result for homotopy elementary types. Homotopy Type Theory 2023. Slides. Pittsburgh, May 2023.
• Weak type theories: a conservativity result for homotopy elementary types. DutchCATS. Amsterdam, May 2023.
• A conservativity-like result for a propositional type theory. 3rd ItaCa Workshop. YouTube Recording. Pisa, December 2022.
• Dialectica: fibrations and logical principles. Applied Category Theory 2022. YouTube Recording. Slides. Glasgow, July 2022.
• Propositional in Dependent Type Theory. Leeds Maths PGR Conference 2022. Leeds, June 2022.
• Towards the notion of Propositional Dependent Sum Types. Proofs, Constructions, Computations and Categories. Leeds, February 2022.
• Dialectica completion & dialectica logical principles. 26th Yorkshire and Midlands Category Theory Seminar. Slides. Birmingham, January 2022.
• Dialectica completion & Gödel fibrations. 2nd ItaCa Workshop. Genoa, December 2021.
• Dialectica logical principles. Eighth Symposium on Compositional Structures. Tallinn, December 2021.
• On the notions of exact completion. Leeds Postgraduate Logic Seminar. Leeds, November 2021.
• Existential, universal and dialectica completion. Proofs, Constructions, Computations and Categories. Leeds, November 2021.
• Regular (first-order) logic symbols & doctrines. Groningen Mathematics PhD Seminar. Groningen, October 2021.
• The Gödel Fibration. Applied Category Theory 2021. Poster. Cambridge, July 2021.
• Quantifier completions of doctrines. Categories and Companions Symposium 2021. YouTube Recording. Sydney, June 2021.

Visiting activities

• ILLC, Amsterdam, the Netherlands. Host Benno van den Berg. April-May 2023.
• University of Padua, Italy. Host Maria Emilia Maietti. December 2022.

Some links and stuff

• Leeds SoM account
• Google Scholar account
• ResearchGate account
• ORCID
• Mathematics Stack Exchange account
• An introduction to doctrines
• An introduction to TQFT
• Master's thesis
• Some sciarade (charades)

A portrait of me and my collaborator working together.