A few other updates:

- This past weekend there was a small workshop at CMU, Bernaysfest, dedicated to the life and work of Paul Bernays, a collaborator of David Hilbert. I snuck in, and heard a bunch of interesting talks on the history of proof theory. (Bernd Buldt's talk, listed as TBA on the schedule, was on "Mathematical practice and platonism: A phenomenological perspective", and quite interesting once I understood what he was trying to do. He wants to give an explanation for why so many mathematicians are platonists, why mathematical objects feel "real" to them, by looking at mathematics as a social process.) The workshop also brought Bill Tait, who last week gave a standing-room-only talk about cut-elimination in predicative systems (Richard Zach blogs about).
- A month ago I gave a fluffy talk on "walking the way of duality" at the Student Seminar Series. Here are the slides, but I'm keeping the video to myself, thank you very much.
- My refinement types paper was accepted to PLPV, as was Dan and Bob's paper, so we'll be going to Savannah.