mastodon 4.7.2assistant professor at Aarhus University interested in (higher) category theory and (modal) type theory. he/him 🏳️🌈
On the advice of (many) friends I asked my doctor to be assessed for ADHD. I... may have mixed in the forms they gave me with my scratch paper (I used them to quickly do a calculation so they had notes on them) which I then used as kindling for a bonfire. I feel like the doctor can't be *that* surprised.
Slides from my talk today at TYPES:
Some news: the first summer school on Programming Languages, Logic, and Software Security, will be held August 10–14, 2026 in Aarhus, Denmark.
The summer school offers intensive courses by leading researchers covering foundational and applied topics at the intersection of programming languages, formal methods, and software security. It is aimed at PhD students and advanced B.Sc./M.Sc. students active in the areas of programming languages, logic, semantics, and software security.
Dates: August 10–14, 2026
Venue: Aarhus University, Aarhus, Denmark
Webpage: https://conferences.au.dk/pls
Courses and Speakers:
Bas Spitters: The Rocq proof assistant and Gen-AI Tools for Formalization of Mathematics
Lars Birkedal and Amin Timany: Higher-Order Concurrent Separation Logic
Daniel Gratzer: Introduction to Type theory
Aslan Askarov: Language-Based Security
Anders Møller: Program Analysis
Looks like I'll be at LICS/FLoC this year. Yay.
Arrived in Gothenburg! Very nice to be back actually... Looking forward to seeing some of you tomorrow at TYPES.
Hey!
Want to come visit Aarhus for a week in August and learn about some fun programming languages stuff? Remember to apply for the PLS summer school (deadline June 7). Some financial support for travel is available!
A note to future me!
I would really love to have the following:
The assignment: \(A : X \to \mathcal{U}\) to
\(\lambda x.\, \bigcirc_{\mathrm{grpd}}\, A\,x : X \to \mathcal{U}\) sends cocartesian families to covariant families.
This seems obvious: the fibers are exactly what you would expect at least. However, it's really hard (for me at least) to understand \(\prod_{i : \mathbb{I}} \bigcirc_{\mathrm{grpd}}A(x\,i) \) in general and to argue that it's covariant.
If anyone wishes to demolish my problem for me, I'd very much appreciate it! It would make a lot of calculations much much easier...
Registration is now open for HoTT/UF 2026! Hope to see some of you in Aarhus soon 😃
See https://hott-uf.github.io/2026/ for registration details.