Ran into Lindsay-from-the-internet there, and her friend Anna, chatted with them for a good while at the little café thingy embedded in Hunt library, where erika showed up again randomly. When did I get so social?
More technical goings-on today included a meeting where
chrisamaphone hashed out her senior thesis draft, and before that a talk by Johnathan Aldrich about an LF-ish proof assistant he's been working on. I'm all for more friendly concrete notation, but I find the treatment of contexts almost as confusing as the way Twelf does it. Maybe it's because Twelf has warped my brain.