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.

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.

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! https://www.dagstuhl.de/en/seminars/seminar-calendar/seminar-details/26121 I gave a talk […]

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

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

This week the #HoTTEST seminar presents: Ayberk Tosun (@ayberkt#hottest 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 […]

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

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

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

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

RE: https://mathstodon.xyz/@de_Jong_Tom/115966213949890726 PSSL deadline for abstracts is *this Friday*. #categorytheory

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. https://sites.google.com/view/pssl112/ Talks at PSSL cover all areas of #categorytheory and its applications. If you'd like to contribute […]

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. https://ploum.net/2026-01-19-exam-with-chatbots.html

I'm pleased that my paper with @MartinEscardo on (counter)examples of injective types is out on arXiv: https://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 […]

RE: https://mathstodon.xyz/@de_Jong_Tom/115791137775475290 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 […]

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 […]

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

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! A great opportunity to make use of @egbertrijke's recently published book, @MartinEscardo's lecture […]

RE: https://mathstodon.xyz/@danielgratzer/115690461702005707 Argh, sorry. But maybe a useful reminder that paper rejections are common, even with good work by (multiple) established people!

The Dutch Functional Programming Day 2026 (also known as the "FP Dag") will be in Nijmegen on Friday, 9 January 2026 https://fpday26.cs.ru.nl

Junk email: "I came across your preprint titled "On Small Types in Univalent Foundations" [...] Your manuscript aligns well with the following journal: Journal of Rare Cardiovascular Diseases" These diseases must indeed be extremely rare if univalent foundations are relevant... 😂

@MartinEscardo 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 […]

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's TypeTopology repository. https://arxiv.org/abs/2501.14542v5 […]

Are you a PhD student registered in a US institution and interested in conducting part of your doctoral research (4-9 months) in France? Then consider applying for a Chateaubriand Fellowship! https://chateaubriand-fellowship.org/

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. Jaap has done a great deal for mathematical logic in the […]

Back from holiday and just caught up on @jonmsterling's very interesting HoTTEST talk titled "Is it time for a new proof assistant?" https://www.youtube.com/watch?v=7oBkEbKJvnE #typetheory

This week I gave a lecture series at the School on Logical Frameworks and Proof Systems Interoperability. I spoke about programming language techniques for proof assistants. The lecture slides and the reference implementations of a minimalist type theory are available at […]

I enjoyed talking about my expository paper (https://doi.org/10.4230/LIPIcs.TYPES.2024.1) at this wonderful CIRM event this morning. https://conferences.cirm-math.fr/3377.html Thanks to Jacopo Emmenegger for the photo! #typetheory #HomotopyTypeTheory #hott

PhD position with Benno van den Berg on the semantics of Homotopy Type Theory (esp. effective Kan fibrations) at the ILLC in Amsterdam! https://www.illc.uva.nl/NewsandEvents/News/Positions/newsitem/15777/PhD-Position-in-the-Semantics-of-Homotopy-Type-Theory Application deadline: 27 September […]

We are advertising a Level D/E position in Pure Maths at University of Adelaide (for non-Oz-initiated: E=full Prof, D=one step down). https://careers.adelaide.edu.au/cw/en/job/517088/associate-professor-professor-de-pure-mathematics

My paper "Continuous and algebraic domains in univalent foundations" with @MartinEscardo was accepted for publication by the Journal of Pure and Applied Algebra! 🎉 https://martinescardo.github.io/papers/continuous-algebraic-domains-in-uf.pdf This paper has its origin in my very first paper with […]

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#logic. I really enjoyed the interaction with all attendees and appreciated […]

ESSLLI 2025 is officially closed! Thank you all so much for being here 🥰 #esslli2025 #logic #language #information #rub

On my way to Bochum to teach a course on Categorical Realizability at the European Summer School in Logic, Language and Information 😄 #esslli2025 #esslli

Two small wins yesterday I have a Word template of a form that I need to complete. Using Word is not fun, especially because the template is relatively complicated, so that, as a Linux user, I'm forced to use a virtual Windows desktop. Small win #1: I found a LaTeX template emulating the Word […]

This is your yearly reminder that anyone who publishes CS papers should have a personal website that lists their current position, research interests, publications, and email address. If you don't, it's basically impossible for me to invite you to a PC […] [Original post on discuss.systems]

TYPES talk done! Time to enjoy the rest of the conference 😄 I talked about injective types in univalent mathematics which is joint work with @MartinEscardo. You can find my slides here https://tdejong.com/talks/TYPES-2025.pdf. #TYPES2025 #typetheory #hott

🚨 #esslli2025 - Last chance for early bird registration (May 31)! 👉 Logic 👉 Language 👉 Information Really interesting courses and the Ruhr area is much more interesting than it is known for! ✨ #nlproc #logic #linguistics #summerschool https://2025.esslli.eu/registration.html

On the first of several trains to CIRM for this nice workshop on semantics of programming languages 😄 https://conferences.cirm-math.fr/3518.html

The abstracts for TYPES 2025 are now available at https://msp.cis.strath.ac.uk/types2025/accepted.html 🎉 I'm involved in two abstracts: (1) "Representing type theories in two-level type theory" with @Nicolai_Kraus (https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper42.pdf); (2) […]

✨European Summer School for Logic, Language and Information 2025✨ in Bochum, Germany: - 47 courses & workshops - 4 exciting evening lectures - social events - explore the Ruhr area Early bird registration deadline: May 31! #esslli2025 #esslli #logic #linguistics #compsci #nlproc #summerschool […]

If you're interested in learning how proof assistants and proof checkers work, and what their underlying formalisms are, consider applying to the International School on Logical Frameworks and Proof Systems Interoperability, which will take place on 8–11 September 2025 in Orsay. France. There […]