Looking for PhD advisors, I recently read Olin Shivers‘ Multi-return Function Call. It’s a really remarkable paper, with all of the attributes of a PL classic. It:
- Proposes a small syntactic extension to the lambda calculus.
- Gives an intuition for how it works and some equivalent, lambda-only constructions.
- Gives an operational semantics.
- Proves the soundness and completeness of a simple type system.
- Proves the soundness and completeness of a parametrically polymorphic type system.
- Designs and proves correct several optimizations for this construct.
- Lists compelling use cases for the new extension.
- Provides an evaluation of the extension as applied to one of those use cases.
I’ve seen a lot of papers which are only the first three, or perhaps four or five. But the last three items are the real kicker. They show that Shivers is really grounded, that he’s not just rambling about Foozles, but is interested in making programming languages better.
If there’s any problem, it’s his writing and way of explaining. Shivers has worked alone a lot, for some unsurprising reasons, so his prose clearly reflects a single person’s thoughts. On the one hand, this makes reading his work a little difficult; on the other, it’s probably the source of a lot of his creativity and incision.
I realized that I mis-cited this paper as being written by Olin Shivers. It is in fact written by Olin Shivers and David Fisher. Still, good stuff: this paper remains a favorite.
I found, and liked this paper by searching for “multiple returns function” and it was exactly what I wanted. I’m not entirely convinced that we should unify ifs and multiple return points, but I’m still digesting.