The theorem proving debriefing lunch was ordered-out mad mex. I had a tasty chicken burrito. Frank seemed to think that all of our projects seemed to contain enough novelty for publication if we really got to polishing them, which kind of surprised me: I knew the group doing bunched logic proving was going out on the frontier quite a bit, but I thought our project was just a matter of doing what had already been done a zillion times. Apparently inverse method with focusing isn't quite as old-hat as I thought.
Tried playing a bit of piano, but my sense of rhythm is really weak today. Read a few articles by Harmon Leon, they're pretty funny.