Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.
Public Key
npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Profile Code
nprofile1qqsd5ct7pm6c9f025rmhq7a7hafqrt3y8hml0aahtj2d92g3xm6x7fqpz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0dsranuz2
Show more details
Published at
2026-05-03T05:29:18Z Event JSON
{
"id": "b876c0f1ea086ba7a466b5cf026627915f626c679902b926e10ecb27561d4c8b" ,
"pubkey": "da617e0ef582a5eaa0f7707bbebf5201ae243df7f7f7b75c94d2a91136f46f24" ,
"created_at": 1777786158 ,
"kind": 0 ,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/de_Jong_Tom",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub"
]
],
"content": "{\"name\":\"Tom de Jong\",\"about\":\"Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.\",\"picture\":\"https://media.mathstodon.xyz/accounts/avatars/109/253/658/214/755/764/original/ab1433c2d1cdbe6d.jpg\",\"banner\":\"https://media.mathstodon.xyz/accounts/headers/109/253/658/214/755/764/original/f4e91639cfa08cad.png\",\"nip05\":\"[email protected] \",\"fields\":[[\"Homepage\",\"https://tdejong.com/\"],[\"GitHub\",\"https://github.com/tomdjong\"]]}" ,
"sig": "1e1325e781f8caf09952f17ebf14650a1d369b97648425963d6f807b69ddbfddd78e173c784a6c52ef3a518a6ee13b66945f49666a90a2f2ebeef4570f55bd11"
}
Last Notes npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong On my way to Gothenburg for #TYPES. Please come and say hi! npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong With apologies for the delay, the recordings of the talks at the Types and Topology Workshop in celebration of @nprofile…t6k2's 60th birthday (https://tdejong.com/mhe60) are now on YouTube (where available) 📺 npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…xuzd As the owner of this weird computer I retract my earlier claim about typst and automatic transitions. (But I still don't know what happened, sorry.) npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong Together with @nprofile…yjy4 and Simona Paoli, I'm organizing the 112th Peripatetic Seminar on Sheaves and Logic (PSSL 112) in Nottingham on 28—29 March 2026.[email protected] by 6 February 2026 (Friday next week). Thanks! npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…xuzd I take it you won't tell us? 🙃 npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong —Abstract— npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong I'm pleased that my paper with @nprofile…t6k2 on (counter)examples of injective types is out on arXiv: https://arxiv.org/abs/2601.12536. npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong The University of Nottingham just enabled Outlook's archive feature: npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong The slides for Types and Topology (https://tdejong.com/mhe60) are all up on the website now (where available)! npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…rrqe For those wondering what's happening in Birmingham: https://tdejong.com/mhe60/ 🙂 npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong I'm happy that my proposal for an introductory course on Homotopy Type Theory / Univalent Foundations at the European Summer School in Logic, Language and Information 2026 in Prague was accepted! npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong Junk email: npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…w8t5 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. npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong 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 @nprofile…w8t5's TypeTopology repository. npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong Following the Heyting Day symposium held in honour of Jaap van Oosten, Benno van den Berg and I wrote a brief popular article on Jaap's life, his scientific work (categorical realizability) and his other contributions to academic life. npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong Back from holiday and just caught up on @nprofile…6kk0's very interesting HoTTEST talk titled "Is it time for a new proof assistant?" npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong PhD position with Benno van den Berg on the semantics of Homotopy Type Theory (esp. effective Kan fibrations) at the ILLC in Amsterdam! npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…6kk0 This basic fact is indeed surprisingly tricky to prove. I think I would follow @nprofile…hszg's approach which goes via Hedberg's argument https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#subsingletonsaresets. npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…6kk0 @nprofile…2pts npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong My paper "Continuous and algebraic domains in univalent foundations" with @nprofile…hszg was accepted for publication by the Journal of Pure and Applied Algebra! 🎉 npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong It was both a pleasure and a privilege to deliver 5 90-min blackboard (!) lectures on Categorical Realizability to 20–30 students and fellow lecturers at the European Summer School in #Logic, Language and Information (#ESSLLI). npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong On my way to Bochum to teach a course on Categorical Realizability at the European Summer School in #Logic, Language and Information 😄 #esslli2025 #esslli npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…v2av "When you say "Next I will do X" or "Now I will do Y" or "I will do X", you MUST actually do X or Y instead just saying that you will do it. npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong This short expository paper has now been published (https://doi.org/10.4230/LIPIcs.TYPES.2024.1) along with the other papers of the TYPES 2024 post-proceedings 🎉 npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…v2av I think the HoTT book did a good job at gently introducing infomal UF. As for your second question: yes, people do write papers in informal UF, e.g. any of @nprofile…hszg's papers (or my own for that matter) where the setting is UF. Not sure if this is a pitfall, but the main thing to be careful about (and which UF forces you to be) is the distinction between property and data, and Sigma and exists. npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…6kk0 Do you have slides you can share? npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong TYPES talk done! Time to enjoy the rest of the conference 😄 I talked about injective types in univalent mathematics which is joint work with @nprofile…hszg. You can find my slides here https://tdejong.com/talks/TYPES-2025.pdf. npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…hszg @nprofile…kkfd There's also the book by Roy Crole, but I haven't read any of it, so I can't say anything more about it really. npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong The recordings and slides of the contributed and invited talks from the Workshop on Homotopy Type Theory/Univalent Foundations (HoTT/UF) are all up at https://hott-uf.github.io/2025/ npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…6kk0 Great, thank you! I'm looking forward to studying this when I'm finished with my ITP reviews... npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…6kk0 Congratulations to all of you! After our discussions, I'm keen to see what you and Leoni did! Will that paper be on arXiv soon? npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong I'm happy to report that my expository note (https://arxiv.org/abs/2408.11501), which has previously been kindly mentioned on here by @nprofile…w52t and @nprofile…6kk0, has been accepted to the TYPES 2024 post-proceedings 🙂 npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong 36th European Summer School in Logic, Language and Information npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong Call for Papers npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…wksm @nprofile…6kk0 I think @nprofile…hszg advises all his PhD students to read this (at least he did to me). npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong @nprofile…6kk0 When I was creating semi-automated marking scripts for Functional Programming (Haskell) assignments, I always had to remember to test for the empty list separately, as many students would forget about it and would fail complete tests just because of the empty list. npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong The Dutch #Categories and #Types Seminar (https://DutchCATS.github.io) yesterday was great fun! npub1mfshurh4s2j74g8hwpama06jqxhzg00h7lmmwhy56253zdh5dujqmu8tlu Tom de Jong —Abstract—
