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

  1. Sharp Elements and Apartness in Domains In EPTCS, volume 351, proceedings of MFPS 2021. December 2021 (submitted June 2021).
  2. 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.
  3. 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).
  4. 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).
  5. 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. 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.
  2. Sharp Elements and the Scott Topology of Continuous Dcpos. Extended version of Publication #1. August 2021.
  3. Domain Theory in Constructive and Predicative Univalent Foundations with Martín Escardó. Extended version of Publication #4. December 2020.

Notes

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

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

  2. Sharp Elements and the Scott Topology of Domains at MFPS 2021, Salzburg (hybrid), 2 September 2021.
  3. 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.

  4. 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.
  5. 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.

  6. Apartness for continuous dcpos (with notes) at BRAVO - Theory PhD students seminar, University of Birmingham, 9 November 2020.
  7. 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.

  8. Constructive domain theory in Univalent Foundations (with notes) at BCTCS 2020, Swansea (held virtually), 8 April 2020.

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

  10. The Scott Model of PCF in Univalent Type Theory (with notes) at TYPES 2019, Oslo, 11 June 2019.

Teaching at University of Birmingham

  1. Exam marker for Theories of Computation (Spring 2022)
  2. TA for Advanced Functional Programming (Spring 2022)
  3. TA for Functional Programming (Autumn 2021)
  4. TA for Theories of Computation (Spring 2021)
  5. TA for Functional Programming (Autumn 2020)
  6. 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)
  7. TA for Network Security (Spring 2020)
  8. TA for Functional Programming (Autumn 2019)
  9. Assistant in Martín Escardó's course on Univalent Type Theory in Agda at the Midlands Graduate School (14-18 April 2019)
  10. Mentor and local co-organizer of the School and Workshop on Univalent Mathematics (1-5 April 2019)
  11. TA for Models of Computation (Spring 2019)
  12. TA for Mathematical Foundations of Computer Science (Autumn 2018)

Miscellaneous

  1. My GitHub page
  2. Some LaTeX packages and tricks I find useful
  3. My power of 10 profile
Last modified on: 22 May 2022.