Jason (jcreed) wrote,

In the morning got more twelf hacking done.

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.
Tags: books, posters, talks, work

  • (no subject)

    Guy from Seattle team we've been working with showed up today at work; no matter how much I'm generally comfortable working with remote teams (and I…

  • (no subject)

    Sean's back in town --- good fun working with nonremote teammates.

  • (no subject)

    Sean's in town at work, good times.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded