mastodon 4.7.2Postdoc at the University of Nottingham working on type theory. PhD from the University of Birmingham. Mathematician, computer scientist and runner.
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.
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.)
#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.
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.
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.]
The slides for Types and Topology (https://tdejong.com/mhe60) are all up on the website now (where available)!
Quoting/Boosting for reach.
On my way to Gothenburg for #TYPES. Please come and say hi!
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
@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
@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
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!
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.
RE: @de_Jong_Tom@mathstodon.xyz
Just over two weeks before early registration ends (31 May)!