Tom de Jong

About    Writings    Talks    Teaching    Misc.    Contact   

Publications

  1. Apartness, sharp elements, and the Scott topology of domains. Mathematical Structures in Computer Science (MSCS), volume 33, issue 7, pp. 573–604. August 2023 (submitted May 2022).
    Extended version of Publication #4.
  2. Set-Theoretic and Type-Theoretic Ordinals Coincide with Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu. July 2023.
    In LICS 2023.
    Publicly available on arXiv: 2301.10696 [cs.LO].
  3. On Small Types in Univalent Foundations with Martín Escardó. Logical Methods in Computer Science (LMCS), 19(2):8:1—8:33. May 2023 (submitted November 2021).
    To be included in the special issue for selected papers of FSCD 2021.
    Extended version of Publication #5.
  4. Sharp Elements and Apartness in Domains In EPTCS, volume 351, proceedings of MFPS 2021. December 2021 (submitted June 2021).
  5. 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.
  6. The Scott model of PCF in univalent type theory. Mathematical Structures in Computer Science, volume 31, issue 10: Homotopy Type Theory 2019, pp. 1270–1300. July 2021 (submitted November 2019).
  7. 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).
  8. 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).
    Included in the special issue Selected papers of the conference "Continuity, Computability, Constructivity – From Logic to Algorithms" (CCC 2018).

Preprints

  1. Formalizing equivalences without tears. August 2024. Expository note.
  2. Domain theory in univalent foundations I: Directed complete posets and Scott's D∞. July 2024.
  3. Domain theory in univalent foundations II: Continuous and algebraic domains with Martín Escardó. July 2024.
    Together with Part I above, this revises and subsumes Preprint #4.
  4. Epimorphisms and Acyclic Types in Univalent Foundations with Ulrik Buchholtz and Egbert Rijke. January 2024. Updated October 2024. To appear in The Journal of Symbolic Logic.
  5. Domain Theory in Constructive and Predicative Univalent Foundations with Martín Escardó. December 2020.
    Extended version of Publication #7.

PhD thesis

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).

Submitted: 30 September 2022.
Defended:  20 December  2022.
Accepted:     1 February    2023.

Official version accepted by the University of Birmingham: https://etheses.bham.ac.uk/id/eprint/13401/.
Also available on arXiv: 2301.12405 [cs.LO]

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.

MSc thesis

My master's thesis on the realizability topos of Scott's graph model was supervised by Jaap van Oosten.
Erratum: The final claim of Proposition 7.1.6 is incorrect: the Sierpiński dominance is not closed under unions. This means that the Frumin–van den Berg framework does not actually apply. See Section 6 of my joint paper with Jaap for further discussion.

Lecture notes

  1. Categorical realizability (March 2024).
    Lecture notes with exercises for an advanced course at the Midlands Graduate School at the University of Leicester, UK.
  2. Domain theory and denotational semantics (March 2023).
    Lecture notes with exercises for an introductory course at the Midlands Graduate School at the University of Birmingham, UK.

Research notes

  1. Constructive taboos involving trichotomous ordinals (April 2022).
    HTML rendering of an Agda formalization with comments.
  2. Semidecidability: constructive taboos, choice principles and closure properties (January 2022).
    HTML rendering of an Agda formalization with comments.
  3. 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.

Outreach

Based on a sketch I made, Jacob Neumann created this research poster for Nottingham's FP Lab. Jacob also made an updated portrait-mode version.
Last modified on 2024-10-31.