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.
News
- June/July 2025: I’m looking forward to returning to the Oregon Programming Languages Summer School to give a lecture series on Category Theory.
- December 2024: I will be speaking at the HoTTEST seminar.
- October 2024: Our paper Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories won the best paper award at APLAS 2024!
- October 2024: Our paper Insights From Univalent Foundations: A Case Study Using Double Categories has been accepted at CSL 2025.
Group
We currently have no PhD or postdoc vacancies.
Current members
Past members
- Alkis Ioannidis, master’s student, 2023-4
- Lukas Mulder, master’s student, 2023-4
- Éléonore Mangel, research intern, 2023-4
- Currently a CS PhD student at Institut de recherche en informatique fondamental
- Dennis Hilhorst, master’s student, 2023
- Erin McCloskey, master’s student, 2020-2
Funding
- From 2021-4, we were funded by the AFOSR.
Research projects
with Nima Rasekh, Niels van der Weide, Benedikt Ahrens
- Insights From Univalent Foundations: A Case Study Using Double Categories, to appear in CSL 2025. [arXiv]
- Univalent Double Categories, published in CPP 2024. [doi] [arXiv]
- Slides from related talks: Informal Formalization
with Dennis Hilhorst
- Formalizing the algebraic small object argument in UniMath, published in ITP 2024. [doi]
- Slides from related talks: ITP
Coalgebraic control of inductive datatypes
with Maximilien Péroux, Lukas Mulder
- Measuring data types (preprint, 2024). [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
Bicategorical type theory
with Benedikt Ahrens, Niels van der Weide
- 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]
Categorical dynamics
with Rob Ghrist, Miguel Lopez, Hans Riess
Structure of the semantics of dependent types
with Benedikt Ahrens, Jacopo Emmenegger, Peter Lefanu Lumsdaine, Egbert Rijke
- Comparing semantic frameworks of dependently-sorted algebraic theories, published in APLAS 2024. [doi]
- Algebraic presentations of dependent type theories (preprint, 2022). [arXiv]
- B-systems and C-systems are equivalent (2023), published in the Journal of Symbolic Logic. [doi]
The univalence principle
with Benedikt Ahrens, Michael Shulman, Dimitris Tsementzis
- The univalence principle (2021), to appear in Memoirs of the AMS. [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
Directed type theory
- 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
PhD thesis: Type theoretic weak factorization systems
- 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
Other papers
- 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]
Teaching
Regular courses
- 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: 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 schools
Activities
Current
Past