Jason (jcreed) wrote,

Class was fine this morning; we just went over how to typecheck System Fω. It was a fine review. I'm very happy I encountered the algorithm for typechecking LF so long ago, because by now the algorithmic equivalence/structural equivalence distinction is deeply baked into my brain, to a dark, golden brown. I kind of did the homework assignment already (implementing exactly that, a typechecker for System Fω) although it hasn't been officially handed out yet. I expect I'll have to search and replace a bunch of times to make my datatype match up with theirs, but probably not that much work more than that.

Researchwise, still wrangling with trying to write down the rules multiplicative and additive function types in this crazy monadic-annotation system in one unified pair of elimination and introduction; the problems that came about led me straight towards the conclusion that actually the additive rules that keep just one world/annotation around everywhere may not really be right. That is, I think they need to mention the inequality after all. fancybred convinced me that they probably aren't directly necessary for the soundness proof, but I think they're necessary for cut elimination to hold.

Did a little bit of work on designing a print for next Tuesday already. Since I was rushed for time last week I tried to get started early. At skamille's suggestion, I'm doing Donner, which is certainly in the running with Wean for most beautifully ugly building on campus. I may be brave enough do a 3 color print instead of the 2-color ones I've done before...

Went to (and "helped set up" in the trivial sense of carrying and opening two whole cases of beer) the "PL area party", a party thrown at Peter Lee's house for the incoming grad students to meet the programming languages students and faculty and such. Of course a lot of them just show up for the food and are apparently quite shameless in admitting it, without the least pretense of excuse that PL is tangentially related somehow to their research interests.

Ditched that after an hour and a half or so and walked down to D's, where I met up with lincoln3, ofsusan, and Susan's brother. Lots of nostalgic discussion of television shows from the '80s ensued.
Tags: classes, printmaking, social, work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded