Matteo Spadetto
Postdoc at the Dipartimento di Scienze Matematiche, Informatiche e Fisiche of the University of Udine, Italy.
My PhD thesis, completed at the School of Mathematics of the University of Leeds (UK), is in mathematical and categorical logic and dependent type theory. It was supervised by Nicola Gambino, Federico Olimpieri, and Michael Rathjen.
Email address. Contact me at matteo.nomen.42@gmail.com where nomen is spadetto.
One of my main research interests lies in the area of homotopy type theory and semantics of dependent type theory. I am particularly interested in propositional (also know in the literature as weak, objective, axiomatic) 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.
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 (arXiv versions here)
- [Preprint] A biequivalence of path categories and axiomatic Martin Löf type theories. October 2024. Together with Daniël Otten.
- [Preprint] Towards propositional dependent sums in intensional and propositional dependent type theory. January 2024.
- [Preprint] Relating homotopy equivalences to conservativity in dependendent type theories with propositional computation [2303.05623v2]. March 2023.
- [Journal paper] Dialectica principles via Gödel doctrines [2205.07093v1]. Theoretical Computer Science. May 2022. Together with Davide Trotta and Valeria de Paiva.
- [Refereed conference paper] Dialectica logical principles [2109.08064v1]. Proceedings of Logical Foundations of Computer Science 2022. September 2021. Extended version → [Journal paper] Dialectica logical principles: not only rules. Journal of Logic and Computation (LFCS 2022 post-conference volume). March 2022. Together with Davide Trotta and Valeria de Paiva.
- [Refereed conference paper] The Gödel fibration. Proceedings of Mathematical Foundations of Computer Science 2021. August 2021. Extended version → [Preprint] The Gödel fibration [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.
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.
A portrait of me and my collaborator working together.