I just spent a fun few days in Glasgow, where I was in town for Malin Altenmüller's (https://maltenmuller.github.io/) successful viva at Strathclyde! I really enjoyed Malin's thesis work and it's always a pleasure to visit the @mspstrath.

I defined enough intrinsically typed MLTT in Agda to give a list append open term in terms of the list inductor, and it's slooooow. Time to write an elaborator, I suppose!

I think it's amazing how briefly Microsoft were the “good guys”. They went from decades of monopolistic practices to “well, unlike all the other computing monopolists, at least they make most of their money the honest way: by developing products and selling them to customers, rather than spying […]

Tomorrow evening, I get to talk to the Philosophy Society students about what I do (as a philosopher/logician) and why I do it. I’ll be interested to discover what the students make of it and where the conversation goes. I love the poster they made for the […] [Original post on hcommons.social]

There are some goings on at the World Othello Championships right now. A couple of years ago, Othello was announced to be weakly solved as a draw, with essentially 5 different proven perfect draw games (see https://arxiv.org/abs/2310.19387). Since that time, the community has come to believe the […]

RE: https://mathstodon.xyz/@egbertrijke/115528036589916180 Congratulations to @egbertrijke on the publication of his textbook on homotopy type theory and univalent mathematics! For many of us classically trained mathematicians, learning univalent mathematics and type theory meant adapting to […]

I guess, when working bidirectionally, explicit substitutions can act as a generalisation of change-of-direction/underline/embedding.

In my blind panic to rid my Firefox installation of LLM integration a while back, I also seemed to knock out all URL bar search suggestions. Not ideal.

So what are the best practices for representing type theories with term-indexed types inside Agda (or equivalent)? Some big inductive-recursive blob containing definitions of weakening and substitution, or is there a nice way to defer them? (I don't care about large elimination or universes – at […]

Some dream code: ``` Check refl. Define refl {xs} : Prefix xs xs by refl <= rec xs { refl : Prefix [] [] := []. refl : Prefix (x :: xs) (x :: xs) := refl :: refl. }. ```

Gif of the day:

If I were making a dependently typed programming language, I'd try to severely deter/restrict the explicit application of implicit arguments. Instead, I would provide an interactive editor command to rephrase the application as a type annotation.

My first encounter with nominative determinism was when I was taught to swim by Mrs Ripley.

The official ads are now out for the #anu #logic Summer School, to be held in #Canberra , Australia from 1-12 December. https://comp.anu.edu.au/lss/ Paraphrasing a bit to fit in a toot: OVERVIEW The ANU Logic Summer School is an annual event that offers a two week long programme of lectures […]

In other transport news, someone from Ipsos is coming round to my house to ask me about public transport this Sunday.

[Edinburgh buses] X33. Tick! ✅

I've lost track of whether I'm snooty about vscode users because of the copious whitespace errors they make, or snooty about whitespace errors because the vast majority come from vscode users.

[Edinburgh buses] A win! As of this week, it seems that the 1 route is fully switched to double-deckers, and moreover battery-powered ones (Volvo BZLs). That and the sudden drop in tourists in September means that they're easily handling the capacity these days.

So, as I understand it, Mercury terms (in the dynamic sense – i.e labelled trees containing unification variables satisfying some inst) never contain more than one copy of any unification variable. This feels like it should be a huge restriction on expressivity – like how affine λ-calculus is […]

[Minute Cryptic] Minute Cryptic - 13 August, 2025 "Even Tom Cruise chases female attention" (5) 🟣🟣🟣🟣🟣🟣🟣🟣 I scored: 2 under par https://www.minutecryptic.com/?utm_source=share

[Minute Cryptic] Minute Cryptic - 12 August, 2025 "House cat got fixed by vet centre" (7) 🟣🟣🟣🟣🟣🟣🟣🟣🟣🟣 I scored: 2 under par https://www.minutecryptic.com/?utm_source=share

[Minute Cryptic] Minute Cryptic - 11 August, 2025 "Gravity department's brief introduction to Hawking" (5) 🟣🟣🟣🟣🟣🟣🟣🟣 I scored: 2 under par https://www.minutecryptic.com/?utm_source=share

[Minute Cryptic] Minute Cryptic - 10 August, 2025 "Server's mistake leads to food arriving unusually late today" (5) 🟣🟣🟣🟣🟣🟣🟣🟣 I scored: 2 under par https://www.minutecryptic.com/?utm_source=share

Small brain: Rejecting intuitionistic logic because the law of excluded middle is obviously true Medium brain: Rejecting intuitionistic logic because its metatheory is ugly and asymmetric Big brain: Rejecting intuitionistic logic because you want comonads and corecursion to work properly

[Minute Cryptic] Minute Cryptic - 9 August, 2025 "Dave stupidly accepted $0.01 for $0.02?" (6) 🟣🟣🟣🟣🟣🟣🟣🟣🟣 I scored: 3 under par https://www.minutecryptic.com/?utm_source=share

[Minute Cryptic] Minute Cryptic - 8 August, 2025 "Song at night club leaves Lucy transfixed by mirrorball?" (7) 🟣🟣🟣🟣🟣🟣🟣🟣🟣🟣 I scored: 4 under par https://www.minutecryptic.com/?utm_source=share

Minute Cryptic - 7 August, 2025 "Hate a self-absorbed flirt" (5) ⚪️🟣🟣🟣🟣🟣🟣🟣 I scored: 1 under par https://www.minutecryptic.com/?utm_source=share

Minute Cryptic - 6 August, 2025 "The one devastated volunteer to miss "One Direction"" (4,4) ⚪️🟣🟣🟣🟣🟣🟣🟣🟣🟣🟣 I scored: 2 under par https://www.minutecryptic.com/?utm_source=share

Minute Cryptic - 5 August, 2025 "Abor_ fr__nd_hip!?" (3,4) ⚪️🟡🟣🟣🟣🟣🟣🟣🟣 I scored: 1 under par https://www.minutecryptic.com/?utm_source=share

The most technologically tricky part of my keyboard layout is also the one I'd most readily recommend to anyone else: putting left shift on the home row (on the caps lock key) and left control just below it.

Each programming language has a “blessèd monad”, which expresses the effects available to all code in the language (often: non-termination, errors, mutation, IO, &c). Maybe it'd be nice in languages with effect type systems to be able to “bless” effects for entire modules or projects – adding […]

Yesterday my first (*) PhD student Riu Rodríguez Sakamoto passed his PhD viva with minor corrections, with a thesis titled "Categorical models in control theory and reinforcement learning". It contained material from our 2 earlier papers "Value iteration is optic composition" ( […]

Should I try to learn the query system used by rustc from rustc (and its developer documentation) itself, or have people written something similar up from a more theoretical/pedagogical perspective? I'm wondering how hard it would be to encode the progress and invariants in indexed types, and […]

I am happy to announce that my colleague Paul Blain Levy has won the Alonzo Church Award. https://siglog.org/winner-of-the-2025-alonzo-church-award/

Morning all! I'm up early today to make a belated appearance at TYPES. My talk is still twice as long as the slot, so please wish me luck for fixing it in the next few hours. 🙏

I'm wondering whether I should change my approach to sound volume settings on my machines. Before, I've generally tried to keep the system master volume at 50%, and adjusted input (i.e application) and output (i.e headphones, speakers) volumes to make this figure comfortable most of the time […]

Great first day of the World Snooker Championship!

Normally unifiability is defined as the existence of a substitution that makes the two terms equal. Is there an equivalent definition that proceeds more structurally on the two terms being unified? Given that the hard part is aliasing, it's really tempting to reach for some sort of separation […]

[Trains] Here's an interesting line of Realtime Trains. The train didn't, in fact, stop – hence the early running.

Pictured: parked car, overhanging parked van, and the shadow cast by the bus from almost perfectly behind, showing its width. Nope, not happening!

I've found a true gem in the talk page for Peirce's law on Wikipedia. It's genuinely the funniest thing I've read in years. 🤣 https://en.wikipedia.org/wiki/Talk:Peirce%27s_law#Current_Explanation_for_Laymen_is_Useless

Here's a fun, 29 SLoC program I thought up at the weekend: https://gist.github.com/laMudri/002d91ffe7e4b093422c25c106127f7f. In short, it seems possible, at least in this simple case, to encode @pigworker's input-subject-output account of bidirectional type checking in the mode system of Mercury […]

I've been having fun times over the past week learning the Mercury programming language. Learning the mode system reminded me a bit of taking Paul Levy's CbPV course, where they take salient (and quite concrete) bits of the semantics and represent them in syntax. Anyway, recommended reading if […]

Remember when repl.it was a website running a collection of REPLs for various programming languages? Well, it's AI now.

Where did I pick up the habit of writing “L/nL” for Linear/non-Linear Logic? It seems that Benton, and most subsequent work, uses “LNL”.

Disaster! I've just noticed that Scotland having a Good Friday bank holiday instead of an Easter Monday bank holiday means we don't get an extra day this year to watch the World Snooker Championship.

Is there a good abstract reason why we seem to get away most of the time with not talking about monomorphisms where we might naïvely have expected to have had to? For example, we can think of pullbacks as a generalisation of intersections from material set theory to arbitrary categories. But if […]

I had a good day writing on the slow train today. In the process, I managed to reduce one definition to the correct level of generality (it was too general before, meaning it contained some junk).

[Trains] The wind has slowed us to a crawl on a pretty bit of the WCML. Too bad the windows haven't been cleaned for years, and are also covered in raindrops.

Manchester is quite windy today, but otherwise seems quite nice in the centre. Is anyone hiring for PL-related R&D there?