Hung out at the Forum for a while with the usual Forumy people. I hope I haven't offended them all horribly with my declining to eat their food. A misoverheard phrase planted the idea of "Klaustuv", the bastard child of Messrs. Sutner and Chaudhuri, in my brain.
In other news, Andrej Bauer was in town and gave the talk for Steve's categorical logic seminar today. Sadly, it wasn't on anything particularly new and flashy that Andrej was working on, just a standard spiel about inductive types being initial algebras. I felt very old every time someone said "Andrej who?" to me when I told them about it.