Tom de Jong

Publications

1. Domain Theory in Constructive and Predicative Univalent Foundations, PhD thesis, University of Birmingham, 2022.
   Supervisor: Martín Escardó, co-supervisor: Benedikt Ahrens.
   Examiners: Vincent Rahli (internal) and Andrej Bauer (external).
   
   Also available as arXiv[cs.LO]:2301.12405
   
   For a very brief overview, please see my viva slides.
   
   If you would like to use a similar LaTeX set up, then you can find a template in my GitHub repository.
2. Sharp Elements and Apartness in Domains In EPTCS, volume 351, proceedings of MFPS 2021. December 2021 (submitted June 2021).
3. Predicative Aspects of Order Theory in Univalent Foundations with Martín Escardó. In LIPIcs, volume 195, proceedings of FSCD 2021. July 2021 (submitted Feburary 2021).
   This won the award for Best Paper by a Junior Researcher.
4. The Scott model of PCF in univalent type theory. Mathematical Structures in Computer Science, volume 31, issue 10: Homotopy Type Theory 2019. July 2021 (submitted November 2019).
5. Domain Theory in Constructive and Predicative Univalent Foundations+ with Martín Escardó. In LIPIcs, volume 183, proceedings of CSL 2021. January 2021 (submitted August 2020).
6. The Sierpinski Object in the Scott Realizability Topos with Jaap van Oosten. Logical Methods in Computer Science (LMCS), 16(3):12:1-12:16. August 2020 (submitted May 2019).

Preprints

1. Set-Theoretic and Type-Theoretic Ordinals Coincide with Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu. January 2023.
2. On Small Types in Univalent Foundations with Martín Escardó. Extended version of Publication #2. May 2022. Submitted upon invitation to the special issue of Logical Methods in Computer Science (LMCS) for selected papers from FSCD 2021.
3. Sharp Elements and the Scott Topology of Continuous Dcpos. Extended version of Publication #1. August 2021.
4. Domain Theory in Constructive and Predicative Univalent Foundations with Martín Escardó. Extended version of Publication #4. December 2020.

Notes

1. Domain theory and denotational semantics (March 2023).
   Lecture notes with exercises for an introductory course at the upcoming Midlands Graduate School at the University of Birmingham, UK.
2. Constructive taboos involving trichotomous ordinals (April 2022).
   HTML rendering of an Agda formalization with comments.
3. Semidecidability: constructive taboos, choice principles and closure properties (January 2022).
   HTML rendering of an Agda formalization with comments.
4. Constructing the circle using propositional truncations and univalence (January 2021).
   HTML rendering of an Agda formalization with comments.
   This formalization largely follows the wonderful paper Construction of the circle in UniMath by Marc Bezem, Ulrik Buchholtz, Daniel R. Grayson and Michael Shulman, although we do not prove the induction principle directly (as is done in Section 4.2 of the paper), but rather derive it abstractly from the universal property of the circle.