Tom de Jong
I am a final-year PhD student at the University of Birmingham in
the
Theoretical Computer Science group.
My supervisor is Martín
Escardó and my co-supervisor is
Benedikt Ahrens .
A copy of my CV .
Contact details
Room 218
School of Computer Science
University of Birmingham
Edgbaston
B15 2TT
Birmingham
United Kingdom
My email address is: t.dejong[symbol]pgr.bham.ac.uk .
Background
I am working on constructive and predicative
domain theory
in
Univalent Foundations .
I obtained a double bachelor's degree in Computer Science and Mathematics at
Utrecht University in 2015.
I 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 .
I have been a PhD student at the University of Birmingham since October 2018.
News
I will be visiting the Faculty of
Mathematics and Physics of the University of Ljubljana from late May to
late June, where Andrej Bauer will host
me.
Publications
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 .
To appear in the special issue
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
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
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.
Talks
Order Theory and Propositional Resizing
in HoTT/UF at
HoTTEST
Event for Junior Researchers 2022 , The Internet, 13 January 2022.
This talk was recorded and is available
on YouTube .
Sharp Elements and the Scott Topology
of Domains at
MFPS 2021 ,
Salzburg (hybrid), 2 September 2021.
Predicative Aspects of Order Theory in
Univalent Foundations at
FSCD 2021 ,
Buenos Aires (held virtually), 22 July 2021.
This talk was recorded and is available on
YouTube .
Predicative Aspects of Order Theory in
Univalent Foundations at
CATS ,
Institute for Logic, Language and Computation (ILLC) of the University of
Amsterdam (online), 16 March 2021.
Domain Theory in Constructive and Predicative
Univalent Foundations at
CSL 2021 ,
Ljubljana (held virtually), 27 January 2021.
This talk was recorded and is available on
YouTube .
Apartness for continuous dcpos
(with notes) at
BRAVO - Theory
PhD students seminar ,
University of Birmingham, 9 November 2020.
Domain theory in predicative Univalent Foundations
(with notes) at
HoTT/UF Workshop 2020 ,
The Internet, 7 July 2020.
This talk was recorded and is available on
YouTube .
Constructive domain theory in Univalent
Foundations (with notes) at
BCTCS 2020 ,
Swansea (held virtually), 8 April 2020.
The Scott Model of PCF in Univalent
Type Theory (with notes) at
CCC 2019 ,
Ljubljana, 5 September 2019.
Please note that this 40-minute talk covers much more than the
15-minute talk (below) at TYPES.
The Scott Model of PCF in
Univalent Type Theory (with notes) at
TYPES 2019 , Oslo,
11 June 2019.
Teaching at University of Birmingham
Exam marker for
Theories of Computation (Spring 2022)
TA for
Advanced Functional Programming (Spring 2022)
TA for
Functional Programming (Autumn 2021)
TA
for
Theories of Computation (Spring 2021)
TA
for
Functional Programming (Autumn 2020)
Co-supervised Brendan Hart with
Martín Escardó on a
final year project
about formalising the Scott model of PCF with variables and λ-abstraction in
Agda . Brendan won the Distinguished Dissertation
Prize for this project.
(Autumn 2019 - Spring 2020)
TA
for Network
Security (Spring 2020)
TA
for Functional
Programming (Autumn 2019)
Assistant in
Martín Escardó 's course on
Univalent Type Theory in Agda
at the Midlands Graduate School (14-18 April 2019)
Mentor and local co-organizer of the
School and Workshop on
Univalent Mathematics (1-5 April 2019)
TA
for Models
of Computation (Spring 2019)
TA
for Mathematical
Foundations of Computer Science (Autumn 2018)
Miscellaneous
My GitHub page
Some LaTeX packages and tricks I find useful
My power of 10 profile
Last modified on: 22 May 2022.