Tom de Jong
About
Writings
Talks
Teaching
Misc.
Contact
Publications
-
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.
-
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. 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).
Preprints
-
Set-Theoretic and Type-Theoretic
Ordinals Coincide with
Nicolai Kraus,
Fredrik Nordvall Forsberg
and Chuangjie Xu. January 2023.
-
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.
-
Sharp Elements and the Scott
Topology of Continuous Dcpos. Extended version
of Publication #1. August 2021.
-
Domain Theory in Constructive
and Predicative Univalent Foundations
with Martín Escardó.
Extended version of Publication #4. December 2020.
Notes
-
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.
-
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.
Last modified on 2023-03-22.