Went to tom7's speaking requirement talk. I think it it was a pretty good presentation; so did the committee, since he passed.
Had an advisor meeting; Frank thinks there's some way to sneak an intuitionistic form of letcc into a dependent type theory and avoid the kind of problems Herbelin outlines in his TLCA '05 paper. I currently don't agree: it looks to me like almost the only leverage you get out of a label-disciplined letcc is that you can't prove classical propositions. Pretty much all the other nice features of intuitionistic provability are tossed out the window.
Just lugged home a few books from the library, among them "Art of Modern Rock", which is fucking amazing. I had seen it in bookstores occasionally, and thought the cover was kind of cheesy --- it's a cartoon pin-up devil-girl on one side, and a sort of angelic version on the other. The guy who did the cover, incidentally, who calls himself "Scrojo" (some of his work is here) uses a lot of nudity and cheap attention-grabbing tricks, but he is still pretty fucking talented. Anyway, the contents of the book are mindblowing to me. So many gorgeous, gorgeous posters, and such an astonishing variety of styles.