Tom de Jong

About me

I am a postdoc at the University of Nottingham in the Functional Programming Lab working on homotopy type theory under the supervision of Nicolai Kraus.

Research interests

I am interested in mathematical structures and logic and their applications to computer science.

Keywords
(homotopy) type theory • univalent foundations • constructive mathematics • category theory • domain theory • realizability • interactive theorem proving and proof assistants (Agda, Lean, Rocq/Coq).

Short bio

From October 2018 until September 2022 I was a PhD student at the University of Birmingham in the Theoretical Computer Science group. My supervisor was Martín Escardó and my co-supervisor was Benedikt Ahrens. My PhD research was on domain theory in constructive and predicative univalent foundations.

Before that, I obtained a double bachelor's degree in Computer Science and Mathematics at Utrecht University in 2015, and completed a research master in Mathematics at the same university in 2018. My master's thesis was on the realizability topos of Scott's graph model and was supervised by Jaap van Oosten.

CV: A copy of my CV.

News

• I am an invited speaker at the Seventh Workshop on Formal Topology which will take place on 13–17 April 2026.
• Our paper Ordinal Exponentiation in Homotopy Type Theory with Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu was accepted to LICS 2025.
  I gave a talk about our paper at the Dutch Categories And Types Seminar.
• My expository paper on equivalences was accepted to the TYPES 2024 post-proceedings.
• Our new preprint with our PhD student Stiéphen Pradal on a study of Kock's fat Delta category is available on arXiv.
• Our paper Epimorphisms and Acyclic Types in Univalent Foundations has been published in The Journal of Symbolic Logic.

Activities

• I was invited to take part in the Proof Systems in Actual Practice: Reasoning and Computation Dagstuhl Seminar on 15–20 March 2026.
• I am excited to be giving a course on Categorical Realizability at ESSLLI in August 2025.
• I joined the TYPES steering committee in June 2024.
• Together with Eric Finster from the University of Birmingham I run the ASSUME seminar series on univalent mathematics.

Past activities

• Programme committees: Interactive Theorem Proving (ITP 2025), TYPES 2025, Certified Proofs and Programs (CPP) 2025, HoTT/UF Workshop 2023.
• Organizing committees: Heyting Day 2025 (held in honour of Jaap van Oosten), HoTT/UF Workshops 2024 & 2025, School and Workshop on Univalent Mathematics 2019.
• At the annual Midlands Graduate Schools, I taught an introductory course on Domain theory and denotational semantics in 2023, and an advanced course on Categorical realizability in 2024.

Mathstodon feed