Tom de Jong
About
Writings
Talks
Teaching
Misc.
Contact
Publications
-
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.
-
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].
-
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.
-
Sharp Elements and Apartness in Domains
In EPTCS,
volume 351, proceedings of
MFPS 2021.
December 2021 (submitted June 2021).
-
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.
-
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).
-
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).
-
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
-
Formalizing equivalences without
tears. August 2024. Expository note.
-
Domain theory in univalent
foundations I: Directed complete posets and Scott's D∞. July 2024.
-
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.
-
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.
-
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
-
Categorical
realizability (March 2024).
Lecture notes with exercises for an advanced course at the
Midlands Graduate
School at the University of Leicester, UK.
-
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
-
Constructive
taboos involving trichotomous ordinals (April 2022).
HTML rendering of an Agda formalization with comments.
-
Semidecidability: constructive taboos, choice principles and closure
properties (January 2022).
HTML rendering of an Agda formalization with comments.
-
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.