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.
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
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