I am an assistant professor at Utrecht University with a dual appointment in the Department of Mathematics and the Department of Information and Computing Sciences. I am also an Honorary Research Fellow in the School of Computer Science at the University of Birmingham and a Guest Researcher at the Delft University of Technology. Previously, I was a postdoc in the Departments of Mathematics and Electrical and Systems Engineering at the University of Pennsylvania, working with Rob Ghrist, and in the Mathematics Department at the Ohio State University, working with Sanjeevi Krishnan. Before that, I did my PhD in mathematics at the University of Cambridge under the supervision of Martin Hyland and my BS in mathematics at the University of Chicago.
In my research, I apply tools of topology and category theory to problems in computer science. I am most focused on the connections between functional programming/type theory and homotopy theory/higher category theory.
- March 2026: I will serve as a PC member for MFPS 2026.
- January 2026: I will serve as a PC member for LICS 2026.
- January 2026: Our paper From Semantics to Syntax: A Type Theory for Comprehension Categories will appear at POPL 2026.
- From 2026-2030, we are funded by an NWO Vidi project.
- From 2021-4, we were funded by the AFOSR.
- Pim Otte, PhD candidate, 2024-
- Fernando Chu Rivera, PhD candidate, 2024-
- Léonard Guetta, postdoc, 2023-
- Alex van Tilburg, master's student, 2025
- Rashiqa Dawood, master's student, 2025
- Stavros Topkas, master's student, 2025
- Alkis Ioannidis, master's student, 2024
- Lukas Mulder, master's student, 2024
- Éléonore Mangel, research intern, 2024
- Dennis Hilhorst, master's student, 2023
- Sylvain Gay, research intern, 2023
- Erin McCloskey, master's student, 2022
with Maximilien Péroux, Lukas Mulder
- Measuring data types (2026), to appear in the postproceedings of CATMI (Category Theory at Work in Computational Mathematics and Theoretical Informatics) 2023 [arXiv]
- Functoriality of Enriched Data Types, published in MFPS 2025. [doi] [arXiv]
- Coinductive control of inductive data types, published in CALCO 2023. [doi] [arXiv]
- Slides from related talks: TYPES, CATMI, CHoCoLa, IRIF, FICS, CMCS, CT, CSCS, Utrecht, HoTTEST
- Videos from related talks: HoTTEST
with Benedikt Ahrens, Niyousha Najmaei, Niels van der Weide
- From Semantics to Syntax: A Type Theory for Comprehension Categories (2026), published in POPL 2026: 2409-2438 (2026) [doi] [arXiv]
- Bicategorical type theory: semantics and syntax (2023), published in Mathematical Structures in Computer Science. [doi] [arXiv]
- Semantics for two-dimensional type theory, published in LICS 2022. [doi]
with Rob Ghrist, Miguel Lopez, Hans Riess
- Categorical Diffusion of Weighted Lattices (preprint, 2025) [arXiv]
- Slides from related talks: Socio-Math, IRIF, Topos Institute, USD
- Videos from related talks: Topos Institute
with Nima Rasekh, Niels van der Weide, Benedikt Ahrens
- Insights From Univalent Foundations: A Case Study Using Double Categories, CSL 2025. [doi] [arXiv]
- Univalent Double Categories, published in CPP 2024. [doi] [arXiv]
- Slides from related talks: Informal Formalization
with Benedikt Ahrens, Jacopo Emmenegger, Peter Lefanu Lumsdaine, Egbert Rijke
- Algebraic presentations of dependent type theories (2025), published in Logical Methods in Computer Science. [doi] [arXiv]
- Comparing semantic frameworks of dependently-sorted algebraic theories, published in APLAS 2024. (Best paper award) [doi] [arXiv]
- B-systems and C-systems are equivalent (2023), published in the Journal of Symbolic Logic. [doi]
with Benedikt Ahrens, Michael Shulman, Dimitris Tsementzis
- The univalence principle (2025), published in Memoirs of the AMS. [doi] [arXiv]
- A higher structure identity principle (2020), published in LICS 2020. [doi] [arXiv]
- Slides from related talks: HoTT, HoTTEST, LICS, Penn Pizza, Algebra | Coalgebra, Penn Logic and Computation Part 1, Part 2, Part 3, MPI, ASL North American Annual Meeting, Utrecht Math, Cornell Topology Festival, (∞,n)-Categories and their applications, Utrecht Philosophy
- Videos from related talks: HoTTEST, LICS
with Dennis Hilhorst
- Formalizing the algebraic small object argument in UniMath, published in ITP 2024. [doi]
- Slides from related talks: ITP
- Towards a directed homotopy type theory, published in MFPS 2019, [doi] [arXiv]
- Slides from related talks: AMS Spring 2018 Central Sectional Meeting, Birmingham, TYPES, HoTT/UF & HDRA, CT, CAS HoTT/UF, MFPS, HoTT-UF, Stockholm, Aarhus, Midwest HoTT, UPenn Applied Topology, Foundations and Applications of Univalent Mathematics, Florida State, Edinburgh, Minisymposium on Physically Grounded Semantics for Programming Hybrid Dynamical Systems, DutchCATS Workshop on AWFSs, GETCO 2022, Paris XIII, Nantes, GETCO 2023, MPI
- Videos from related talks: Spring School on Theoretical Computer Science (EPIT) – Homotopy Type Theory, Edinburgh, Minisymposium on Physically Grounded Semantics for Programming Hybrid Dynamical Systems, DutchCATS Workshop on AWFSs, GETCO 2022
- Identity types and weak factorization systems in Cauchy complete categories, (2019), published in Mathematical Structures in Computer Science. [doi] [arXiv]
- Type theoretic weak factorization systems, PhD thesis, 2017, University of Cambridge [doi]
- Slides from related talks: JMM, Leeds
- A Hurewicz model structure for directed topology (2021), joint with S. Krishnan, published in Theory and Applications of Categories. [tac] [arXiv]
- Univalent foundations and the equivalence principle (2019), joint with with B. Ahrens, published in Reflections on the Foundations of Mathematics, Synthese. [doi] [pdf]
- Spring 2026: Software testing and verification (Utrecht)
- Spring 2026: Homotopy type theory (Mastermath)
- Spring 2025: Seminar on Logic and Foundations of Computing (Utrecht)
- Spring 2025: Homotopy type theory (Mastermath)
- Winter 2024: Logica voor informatica (Utrecht)
- Spring 2024: Advanced functional programming (Utrecht)
- Spring 2024: Homotopy type theory (Mastermath)
- Spring 2023: Softwareproject informatica (Utrecht)
- Spring 2023: Advanced Mathematics (University College Utrecht)
- Autumn 2021: Calculus III -- linear algebra (Penn)
- Spring 2021: Calculus IV -- applied partial differential equations (Penn)
- Spring 2020: Foundations of Higher Mathematics (OSU) (videos)
- Autumn 2018: Linear Algebra (OSU)
- Spring 2018: Introduction to Discrete Mathematics (OSU)
- Autumn 2017: Linear Algebra (OSU)
- Lent 2015: Number Fields (Cambridge)
- Michaelmas 2014: Galois Theory (Cambridge)
- Michaelmas 2012: Number Theory (Cambridge)
- Summer 2025: Utrecht Summer School on Geometry
- Summer 2025: Escuela de Ciencias Informáticas
- Summer 2025: Oregon Programming Languages Summer School
- Summer 2024: UniMath School
- Fall 2023: Interactions of Proof Assistants and Mathematics (materials)
- Summer 2023: Oregon Programming Languages Summer School (materials)
- Summer 2022: Applied Category Theory Adjoint School
- Summer 2022: HoTTEST Summer School
- Summer 2022: UniMath School
- Spring 2021: Spring School on Theoretical Computer Science (EPIT) (video)
- Summer 2020: Applied Category Theory Adjoint School
- Summer 2019: Ross Program (course page)
- Organizer of DutchCATS
- Organizer of the Formalizing Higher Categories workshop at the Mittag-Leffler Institute
- Inaugural member of the Homotopical Algebra and Higher Category Theory from Foundations to Applications EMS TAG (European Mathematical Society Topical Activity Group)
- PC Member of MFPS 2023, 2026
- PC Member of LICS 2026
- PC Member of HoTT/UF 2017, 2020, 2021, 2022, 2023, 2026
- PC Member of TYPES 2026
- PC Member of POPL 2026
- Steering committee chair of TYPES (2023-5)
- PC Member of ACT 2022, 2023, 2024
- PC Member of STACS 2024
- PC Member of CPP 2024
- PC Member of SYCO 11, 12
- Organizer of WG6 2023 Meeting
- PC Member of MFPS 2023
- Scientific organizer of HoTT/UF 2022
- Organizer of Midwest HoTT Seminar 2020 (cancelled)