"Resource usage analysis", Igarishi and Kobayashi, from POPL'02. This was the PLClub paper of the week. I didn't care for it much at all. There's some idea in there that seems really cool as a generalization of linear uses, but I struggled in vain to really grasp it. There are too many formal concepts not really nailed down enough for me to understand what they're doing. There's not really a strong distinction between things that are definitely propositions and things that are merely functions-on-propositions that feels incredibly alarming to me aesthetically. I'm told these are the dudes who went on to do session types --- can't say I ever totally understood them, either.
"Simplicial Databases", David Spivak. Got this from a CMU talk announcement that Steve Awodey sent out. I am such a sucker for aiming big, big categorical guns at problems like these. I kind of lost track of what was going on halfway through, but it was fun going up to that point, pullbacks and slice categories and labelled simplicial categories and whatnot, all in the name of making mathematical sense out of how databases are actually done out in the real world, especially when that diverges from the nice but too-simplistic classical theory of relational algebra.
"F-ing modules", Andreas Rossberg, Claudio Russo, and Derek Dreyer. This paper is an utter breath of fresh air. I like it so much I find myself constantly worrying that I am missing some flaw in it only because of my nonexpertise in module systems research. Anyhow I find it a rarity that I am able to write a research paper in such a pleasantly direct style. It's just, I don't know, here is what we are going to do, here is why we want to do it, here is how it works, step one, two, three, there --- we're done, isn't it fucking beautiful? Maybe it is a matter of choosing your content carefully to be in reasonably-sized pieces or something, but even before finishing digesting all the middle bits, I can already say that I find it a pleasure to read, and a very nice result to boot, to wit, directly translating a generalization of the ML module system into System Fω. I mean, if there are not the aforementioned flaws that I am too dumb to notice, it definitely has the feeling of "gosh why wasn't the ML module system explained this way all along" to it. You just kind of pop out abstract types into "monadically" managed prefixes of System Fω existential quantifiers and dodge a ton of bullshit with selfification and the avoidance problem and stuff.
Plus, you can't beat the cute title.
