Matteo Spadetto

Before joining Gallinette, I was a postdoc at the Dipartimento di Scienze Matematiche, Informatiche e Fisiche of the University of Udine, Italy, supervised by Marino Miculan.

My PhD thesis, completed at the School of Mathematics of the University of Leeds (UK), is in mathematical logic, dependent type theory, and categorical semantics. It was supervised by Nicola Gambino, Federico Olimpieri, and Michael Rathjen.

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] 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 dependent type theories with computation axioms. Logical Methods in Computer Science. September 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] The biequivalence of path categories and axiomatic Martin Löf type theories. [2503.15431]. Accepted for Computer Science Logic 2026. October 2024. Together with Daniël Otten.
[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

Me and my collaborator working together: one is deaf until the other begins to speak.