transatlantic updates

So I just arrived in Paris today. Last week I was in Nottingham at DTP, then visiting my sister in London. Both were awesome! In my talk at DTP, I began with some ludics propaganda, then tried to walk the audience through how to encode focusing with higher-order rules in Agda (and extract a functional programming language with explicit evaluation order and pattern-matching). You can check out the annotated agda code. I also had/overheard lots of great conversations, in particular Sebastian Hanowksy taught me some fascinating things about synthetic topology and the delay monad, and Anton Setzer/Peter Hancock piqued my interest in going back to Buchholz's work about the ω/Ω-rule. The highlight of the London visit was probably seeing Chango Spasiuk.

This week I'll be meeting with Paul-André Mellies, and giving talks at PPS and LIX.