Elektrine
EN
Log in Register
Paige Chat Timeline Communities Gallery Videos Email DNS VPN Uptime Kairo
Back to Timeline
Remote

Tom de Jong

@de_Jong_Tom@mathstodon.xyz
mastodon 4.6.4
  • Open on mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

0 Followers
0 Following
24 Posts
Joined October 29, 2022
Homepage:
https://tdejong.com/
GitHub:
https://github.com/tomdjong

Posts

Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · May 12, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @chrisTheClimber@mathstodon.xyz
@chrisTheClimber@mathstodon.xyz This really depends on your specific background and how far you'd be travelling and so on. I would say that the important thing is that you're excited. Even if you can't follow all of the talks, I'm sure people would be happy to talk to you, I certainly would! @matematiflo@mathstodon.xyz @mevenlennonbertrand@lipn.info
1
2
0
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · May 12, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

RE: @de_Jong_Tom@mathstodon.xyz

Just over two weeks before early registration ends (31 May)!

mathstodon.xyz

Tom de Jong: "The 37th European Summer School in Logic, Languag…" - Mathstodon

1
0
5
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · May 09, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

As usual, I was reading this weekend's De Volkskrant (Dutch newspaper) and amused to find @jonmsterling@mathstodon.xyz quoted in @ionica@mathstodon.xyz's column 🙂

(Minor correction to the column: Jon isn't British.)

mathstodon.xyz

Jon Sterling (@jonmsterling@mathstodon.xyz) - Mathstodon

22
10
4
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · May 09, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @matematiflo@mathstodon.xyz
Definitely agree! On both statements :) @matematiflo@mathstodon.xyz @jeanas@mathstodon.xyz @mevenlennonbertrand@lipn.info
2
0
0
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · May 08, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

#TYPES 2026 is done! The slides for my talk are here: https://tdejong.com/talks/TYPES-2026.pdf.
Joint work with @ljungstrom@mathstodon.xyz and @Nicolai_Kraus@mathstodon.xyz.

mathstodon.xyz

Mathstodon

14
2
7
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · May 03, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

On my way to Gothenburg for #TYPES. Please come and say hi!

mathstodon.xyz

Mathstodon

8
0
1
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Apr 23, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @gadmm@mathstodon.xyz
@gadmm@mathstodon.xyz I don't really have additional information, sorry. Maybe some of the #agda developers would like to chime in, but I'd understand it if they don't.
2
3
0
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Apr 23, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

RE: @jaror@social.edu.nl

Quoting/Boosting for reach.

9
5
1
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Apr 22, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @dif@mathstodon.xyz
@dif@mathstodon.xyz The recordings were made private until some explicit permission is given via some forms which are yet to be send out. However, I'm not even sure that my talk was successfully recorded, as I never saw it listed (unlike the other talks). @nmvdw@mathstodon.xyz
0
1
0
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Apr 20, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @ionchy@types.pl
@ionchy @andrejbauer I'm not getting the typst hate either. In particular I've found its documentation to be quite reasonable.
3
3
0
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Apr 20, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

The 37th European Summer School in Logic, Language and Information
(ESSLLI 2026) will take place on 3-14 August in Prague.
https://2026.esslli.eu

I'm excited that I'll be teaching an introductory course on univalent foundations / homotopy type theory!

@stringdiagram@mathstodon.xyz and @jaklt@mastodon.social will also be running an interesting workshop titled "Semantics and compositionality for expressiveness and complexity".

Early registration closes on 31st May.

16
0
13
2
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Apr 17, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

At 9.50 today, I'm giving a talk on constructive domain theory at the Formal Topology Workshop in Venice. Feat. a shoutout to @nmvdw@mathstodon.xyz and @dif@mathstodon.xyz for their nice paper "The Interval Domain in Homotopy Type Theory".

It should be livestreamed: @wires0@youtube.com
[Update: it seems the recording of my talk failed.]

Slides: https://tdejong.com/talks/7WFTop.pdf

mathstodon.xyz

Niels van der Weide (@nmvdw@mathstodon.xyz) - Mathstodon

12
3
7
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Apr 16, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

I'm pleased, especially for our PhD student @aref_mz@mathstodon.xyz, that our paper "Generalized Decidability via Brouwer Trees" (https://arxiv.org/abs/2602.10844) with @aref_mz@mathstodon.xyz, @Nicolai_Kraus@mathstodon.xyz and @fnf@mathstodon.xyz was accepted to LICS'26.

#Agda was very useful for developing this work. Huge thanks to its maintainers!

My commiserations to those who submitted good work but didn't get in. I hope we can all escape this system one day.

mathstodon.xyz

Aref Mohammadzadeh (@aref_mz@mathstodon.xyz) - Mathstodon

43
0
18
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Apr 09, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @danielgratzer@mathstodon.xyz
@danielgratzer OK, thanks! And sorry I can't make it in person 😔
2
0
0
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Apr 09, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @danielgratzer@mathstodon.xyz
@danielgratzer Will there be (limited) options for remote participation? (I believe the original calls mentioned this, but might be wrong.) If so, should remote participants register too?
2
3
0
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Mar 31, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

Thanks to our speakers and @Stiephen@mathstodon.xyz all the slides for PSSL 112 are now available on the PSSL website! https://sites.google.com/view/pssl112/program

#CategoryTheory #Logic

mathstodon.xyz

Stiephen Pradal (@Stiephen@mathstodon.xyz) - Mathstodon

11
0
2
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Feb 27, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @dwarn@mathstodon.xyz
@dwarn Thanks for elaborating! I've thought about this before, but it's funny how fruitful incorrect proofs/claims tend to be for coming up with (correct proofs of) interesting results. @MartinEscardo
1
0
0
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Feb 27, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @dwarn@mathstodon.xyz
@dwarn Here's a question that I can't answer: how did you come up with this?! Now that I've finished my file, I can explain the result and why it holds, but this is relatively easy because it's post-fact. It only worked because I knew it was true and could look up critical steps in your formalization. @MartinEscardo
5
2
0
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Feb 27, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @de_Jong_Tom@mathstodon.xyz

@MartinEscardo @dwarn Here's my account: https://martinescardo.github.io/TypeTopology/gist.ThereAreNoHigherSemilattices2.html

My main take-away is the following observation. A loop space is trivial if it can be equipped with a binary operation ⋆ such that

  • it has an interchange law: (p ⋆ q) ∙ (r ⋆ s) = (p ∙ r) ⋆ (q ∙ s);
  • it is idempotent, commutative and associative.

Proving that an idempotent, commutative and associative binary operation on a pointed type induces such an operation ⋆ on its loop space is then quite tricky when it comes to commutativity and associativity. I elaborated David's argument as follows: first prove that ⋆ is commutative up to conjugation, then use idempotency to show that conjugation acts trivially, so that ⋆ really is commutative (without conjugation), and similarly (but slightly more involved) for associativity.

The intellectual credit naturally lies with David, but hopefully my elaboration/account is helpful for others too!

6
4
2
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Feb 25, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @MartinEscardo@mathstodon.xyz
@MartinEscardo @dwarn To really understand it, I've been working on my own retelling. If I manage to complete it, I'll share it here. Thanks to both of you for sharing!
3
5
0
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Feb 24, 2026
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz
Replying to @OscarCunningham@mathstodon.xyz
@OscarCunningham I don't know about the MO question, but suplattices have a prop-valued reflexive and antisymmetric relation and any type with such a relation is necessarily a set. This can be seen with a much simpler argument using what @MartinEscardo calls local Hedberg. https://martinescardo.github.io/TypeTopology/UF.HedbergApplications.html#2299 @dwarn
3
1
1
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Dec 18, 2025
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

The slides for Types and Topology (https://tdejong.com/mhe60) are all up on the website now (where available)!

@MartinEscardo@mathstodon.xyz

25
2
17
1
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Oct 24, 2025
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

@MartinEscardo@mathstodon.xyz is turning 60 this year! In celebration, Eric Finster and I are organizing a two-day workshop on 17-18 December 2025 at the University of Birmingham.
https://tdejong.com/mhe60

The full list of over 20 invited speakers can be found on the website and reflects Martín's diverse contributions to constructive mathematics, domain theory, locale theory, logic, topology and homotopy/univalent type theory.

The workshop is co-located with the Midlands Graduate School (MGS) Christmas Seminar on 16 December 2025 and will support remote participation.

If you would like to attend (in person or remotely), please register by
*21 November 2025* by completing this form:
https://forms.cloud.microsoft/e/4GgaZHTxad

29
1
21
0
Open post
de_Jong_Tom
Tom de Jong @de_Jong_Tom@mathstodon.xyz · Oct 22, 2025
Tom de Jong
@de_Jong_Tom@mathstodon.xyz

Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.

mathstodon.xyz

The extended version of our LICS'25 paper, titled Constructive Ordinal Exponentiation, is now on arXiv. It has two new sections (Section 6 and 8) on ordinal arithmetic. Everything is formalized in Agda and merged into @MartinEscardo@mathstodon.xyz's TypeTopology repository.
https://arxiv.org/abs/2501.14542v5

This joint work with @fnf@mathstodon.xyz, @Nicolai_Kraus@mathstodon.xyz and Chuangjie Xu.

#TypeTheory #logic #Agda

13
0
8
0

Remote instance

mathstodon.xyz
Open on original server

Media

313k7r1n3
Elektrine

Tor hidden service

elekhj7afj4qnrr4yd3bkzslsyo5jgfxw3orgjkhlcxifueodybyiiad.onion

Platform

  • Email
  • Chat
  • Timeline
  • Communities
  • VPN
  • DNS

Company

  • About
  • Contact
  • FAQ

Legal

  • Terms of Service
  • Privacy Policy
  • Warrant Canary
  • Lite (no JS)
  • VPN Policy
  • Source code

Support

  • support@elektrine.com
  • Report Security Issue
Mail client setup IMAP mail.elektrine.com:993 POP3 mail.elektrine.com:995 SMTP mail.elektrine.com:465
© 2026 Elektrine. All rights reserved. Server: 04:22:24 UTC