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. 