iiinova — where your digital self keeps evolving

Tom de Jong

@de-Jong-Tom.mathstodon.xyz.ap.brid.gy

51 followers 2 following 96 posts

Postdoc at Radboud University, previously at University of Nottingham, working on type theory. PhD from University of Birmingham. Mathematician, computer […] 🌉 bridged from ⁂ mathstodon.xyz/@de_Jong_Tom, follow @ap.brid.gy to interact

Posts Replies Media

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 05/10/2026

This week the #HoTTEST seminar presents: Steve Awodey Path types in Algebraic Type Theory The talk is at 11:30am EST (16:30 UTC) on Thursday, October 8. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See hottest-seminar.github.io for the Zoom link and a […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 01/10/2026

I've started my new job! As of today, I'm a postdoc in the Software Science group of the Institute of Computing and Information Sciences at Radboud University in the Netherlands. This position is (largely) funded by a personal 3-year Veni fellowship from the Dutch research organization NWO. I'm […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 19/09/2026

The slides for my course in homotopy type theory / univalent foundations at the Proof and Computation autumn school are available at: tdejong.com/talks/PC-2026-1.pdf tdejong.com/talks/PC-2026-2.pdf tdejong.com/talks/PC-2026-3.pdf As always it was a great pleasure to be a […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 18/09/2026

[LLMs] I'm not big on legalese but nevertheless I found this court document [1, found via [2]], and the quotes from people in the tech industry, quite interesting. Example: "Microsoft has observed that “threaten[ing] the economic foundations of its essential […] [Original post on mathstodon.xyz]

Picture from a Microsoft document with the caption "Argument from Data Leverage literature: We tech folks might think we're the entire world, but content creators are Archimedes."

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 09/09/2026

RE: mathstodon.xyz/@de_Jong_Tom/1159326… And now this paper with @MartinEscardo on injective types is published in the Annals of Pure and Applied Logic 🙂️ doi.org/10.1016/j.apal.2026.103829

000

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 15/08/2026

RE: mathstodon.xyz/@de_Jong_Tom/1168962… Teaching homotopy type theory in just 5 lectures was certainly a challenge, but also a hugely enjoyable one! Many, many thanks to all that attended and their lovely questions! I had a fantastic time in Prague where I also enjoyed […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 15/08/2026

RE: links.bouncepaw.com/2290 This was a fun read

links.bouncepaw.com

000

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 13/08/2026

Who came up with the "type check" vs "vibe check" joke? The students in my HoTT course liked it, and I also like it a lot (and it's actually useful in some explanations). But I would like to remember who came up with it, so that I can give them credit in the future.

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 09/08/2026

Made to Prague for #ESSLLI! The hotel room TV remote is interesting 😄

A remote with a lambda on the bottom left.

Reposted by Tom de Jong

Gro-Tsen @gro-tsen.bsky.social · 07/08/2026

I asked a long question on MathOverflow about which topos best represents L. E. J. Brouwer's ideas on intuitionism (some of which I have tried to summarize): mathoverflow.net/q/514026/17064

mathoverflow.net

Which topos (or topoi) most accurately reflect Brouwer's ideas on intuitionism?

Let me first clarify that I am not expecting the titular question to have a single well-defined answer (or it would probably have to be a useless one like “the topos freely generated by the followi...

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 03/08/2026

Just learnt that our paper "A study of Kock's fat Delta" (arxiv.org/abs/2503.10963) with Nicolai Kraus (@Nicolai_Kraus), Simona Paoli and Stiéphen Pradal (@Stiephen) was accepted for publication in the Journal of Pure and Applied Algebra (JPAA). I'm quite happy about this, but I'm […]

Original post on mathstodon.xyz

000

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 23/07/2026

One of the joys of using #Typesetter (a minimal editor for #typst) is that I find it improves after each update which is not usually the case for many other pieces of software 🥲️

Reposted by Tom de Jong

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 15/07/2026

I was invited to speak at the Summer Conference on Topology 2026and its Applications in Split, Croatia. This is how I tried to explain the topos of countable reals to ordinary topologists: www.andrej.com/assets/slides/topolo… I did get a bunch of […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 10/07/2026

The teaching materials (first version) for my course "Introduction on Homotopy Type Theory / Univalent Foundations" at ESSLLI 2026 are now available at github.com/tomdjong/ESSLLI-2026 I really enjoyed putting this together and naturally I (re)learnt a thing or two myself in the […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 22/06/2026

This week I'm very much looking forward to the "Formal proof and synthetic mathematics" workshop co-organized by @matematiflo! matematiflo.github.io/ProofWorkshop… Can't say the same about the weather forecast...

000

Reposted by Tom de Jong

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 14/04/2026

I'm on the PC of Computer Science Logic (CSL 2027). csl2027.github.io The abstract/paper submission deadlines are 8/15 July 2026 (AoE) with notification of accepted papers on 15 October 2026, and the conference itself on 25-29 January 2027 in Brighton. I would love to see papers on […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 04/06/2026

RE: mathstodon.xyz/@de_Jong_Tom/1164356… The early-bird registration deadline for the European Summer School in Logic, Language and Information (ESSLLI) has been extended to 15 June. 2026.esslli.eu/registration/registr… [More details in the reply to this post.]

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 03/06/2026

Does anybody know how to typeset pullback/pushout corners in typst/fletcher? The code provided at github.com/Jollywatt/typst-fletcher… does not quite work for me and even when it does, it requires experimenting with degrees which is bad. #typst […]

Original post on mathstodon.xyz

000

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 01/06/2026

RE: mathstodon.xyz/@iblech/116675413147… I didn't know of this collection of notes by (the late) Thomas Streicher. Thanks for sharing them! www2.mathematik.tu-darmstadt.de/~st…

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 15/05/2026

RE: mathstodon.xyz/@de_Jong_Tom/1160756… Application deadline: 1 June. This year's edition will be the 10th!

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 12/05/2026

RE: mathstodon.xyz/@de_Jong_Tom/1164356… Just over two weeks before early registration ends (31 May)!

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 09/05/2026

As usual, I was reading this weekend's De Volkskrant (Dutch newspaper) and amused to find @jonmsterling quoted in @ionica's column 🙂 (Minor correction to the column: Jon isn't British.)

Partial screenshot of Ionics Smeets' column (in Dutch) that quotes Jon Sterling.

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 08/05/2026

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

000

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 03/05/2026

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

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 23/04/2026

RE: social.edu.nl/@jaror/11645369030424… Quoting/Boosting for reach.

000

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 20/04/2026

Following @jaycech3n's beautiful PSSL 112 slides (drive.google.com/uc?export=download…) I tried out typst last week. Verdict: For papers, LaTeX (after all, I'll want to submit them). For anything else, typst.

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 20/04/2026

The 37th European Summer School in Logic, Language and Information (ESSLLI 2026) will take place on 3-14 August in Prague. 2026.esslli.eu I'm excited that I'll be teaching an introductory course on univalent foundations / homotopy type theory! @stringdiagram and @jaklt will also be […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 19/04/2026

RE: types.pl/@ncf/116427482324540411 Fun puzzle and a nice observation!

000

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 17/04/2026

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 and @dif for their nice paper "The Interval Domain in Homotopy Type Theory". It should be livestreamed: youtube.com/@wires0/streams Slides […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 16/04/2026

I'm pleased, especially for our PhD student @aref_mz, that our paper "Generalized Decidability via Brouwer Trees" (arxiv.org/abs/2602.10844) with @aref_mz, @Nicolai_Kraus and @fnf was accepted to LICS'26. #Agda was very useful for developing this work. Huge thanks to its maintainers! […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 14/04/2026

I'm on the PC of Computer Science Logic (CSL 2027). csl2027.github.io The abstract/paper submission deadlines are 8/15 July 2026 (AoE) with notification of accepted papers on 15 October 2026, and the conference itself on 25-29 January 2027 in Brighton. I would love to see papers on […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 13/04/2026

RE: mathstodon.xyz/@buchholtz/116397805… Me too! 😁

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 31/03/2026

Thanks to our speakers and @Stiephen all the slides for PSSL 112 are now available on the PSSL website! sites.google.com/view/pssl112/progr… #CategoryTheory #Logic

The participants of PSSL 112 are standing on a patch of grass in sunny conditions.

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 29/03/2026

I recently spent considerable time and effort subreviewing a paper (I could afford to). I'm really, really pleased to see that this was appreciated by the author and will lead to an improved paper.

000

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 28/03/2026

Paul Levy at PSSL 112: "Unfortunately... Or rather, sadly, there's no fortune when it comes to maths." Maybe I should dedicate my account to Paul Levy quotes.

000

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 20/03/2026

I had a great time at this Dagstuhl seminar on proof assistants and constructive/synthetic mathematics. Many thanks to the organizers Ingo Blechschmidt, Liron Cohen, Thierry Coquand, and Peter Schuster! www.dagstuhl.de/en/seminars/seminar… I gave a talk […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 07/03/2026

RE: mathstodon.xyz/@ayberkt/11617821363… And the recording is on YouTube: youtu.be/3jk1INJgcqs Thanks again, @ayberkt!

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 04/03/2026

The program for the 112th Peripatetic Seminar on Sheaves and Logic (PSSL 112) is up on the website sites.google.com/view/pssl112/progr… 17 talks on #CategoryTheory (and #TypeTheory) from a variety of speakers! If you'd like to attend please register by March 14th following the form on […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 03/03/2026

This week the #HoTTEST seminar presents: Ayberk Tosun (@ayberkt) Constructive and predicative locale theory in univalent foundations The talk is at 11:30am EST (16:30 UTC) on Thursday, March 5. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 20/02/2026

I'm on the PC of MFPS (Mathematical Foundations of Programming Semantics) this year. ul-fmf.github.io/mfps-sstt-2026/mfp… Please consider submitting a paper, especially if it's on constructive mathematics, domain theory, denotational semantics and/or (homotopy) type […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 15/02/2026

The 2026 website for the annual autumn school Proof and Computation is now up at www.mathematik.uni-muenchen.de/~sch… I'm excited to give a short course introducing homotopy type theory / univalent foundations, and look forward to participating in this very enjoyable school […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 13/02/2026

With apologies for the delay, the recordings of the talks at the Types and Topology Workshop in celebration of @MartinEscardo's 60th birthday (tdejong.com/mhe60) are now on YouTube (where available) 📺 www.youtube.com/@mhe60/videos (also linked from the workshop webpage) Many […]

Original post on mathstodon.xyz

Reposted by Tom de Jong

Noam Zeilberger @noamzoam.mathstodon.xyz.ap.brid.gy · 12/02/2026

The arXiv's new "make everyone write in English to promote linguistic diversity" policy went into effect yesterday (blog.arxiv.org/2026/01/13/non-engli…), and they have now released a feedback survey […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 03/02/2026

RE: mathstodon.xyz/@de_Jong_Tom/1159662… PSSL deadline for abstracts is *this Friday*. #CategoryTheory

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 27/01/2026

Together with @Stiephen and Simona Paoli, I'm organizing the 112th Peripatetic Seminar on Sheaves and Logic (PSSL 112) in Nottingham on 28—29 March 2026. sites.google.com/view/pssl112 Talks at PSSL cover all areas of #CategoryTheory and its applications. If you'd like to contribute […]

Original post on mathstodon.xyz

Reposted by Tom de Jong

ploum @ploum.mamot.fr.ap.brid.gy · 19/01/2026

Giving University Exams in the Age of Chatbots How I managed to give an exam while giving the students the choice to use a chatbot or not. And what I learned in the process. ploum.net/2026-01-19-exam-with-chat…

Giving University Exams in the Age of Chatbots

Giving University Exams in the Age of Chatbots par Ploum - Lionel Dricot.

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 21/01/2026

I'm pleased that my paper with @MartinEscardo on (counter)examples of injective types is out on arXiv: arxiv.org/abs/2601.12536. This paper took a while to come together, partly because we refined the exposition a few times, partly because we kept coming up with new (counter)examples […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 02/01/2026

RE: mathstodon.xyz/@de_Jong_Tom/1157911… The new year starts off right! A few days ago I described my trouble with Microsoft's In-Place/Online Archive in the quoted post. I'm very happy that I can access my old emails through Thunderbird again thanks to DavMail and a nudge by […]

Original post on mathstodon.xyz

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 27/12/2025

The University of Nottingham just enabled Outlook's archive feature: To keep your mailbox lighter and faster, emails that are older than 90 days are automatically moved into an online archive. You will find your old emails in the following folder: - In the Outlook app, the folder name is […]

Original post on mathstodon.xyz