Undergraduate-level computer science can feel disjointed at times: for example, at that level, one feels that operating systems and programming languages are entirely separate subdisciplines, whose practitioners have apparently never spoken to one another. The same feeling repeats itself with the more advanced topics of complexity and type theory. Unfortunately, graduate-level computer science does little to dispel that, although with sufficient digging in the research literature, one can see some intersection between operating systems and programming languages.

The intersection between type theory and computational complexity is much harder to see, although it is there. This paper shows beautifully how rich it is. It turns out that there is a direct correspondence between polymorphic functions on finite types and basic complexity classes. In fact, much more is true: higher-order primitive recursive functions precisely capture basic complexity classes. This is an absolutely phenomenal result.

Furthermore, the exposition of these results is a joy to read. The author provides a solid introduction to the necessary concepts, deftly balancing rigor and intuition. All of the most important ideas are illustrated with examples, and the crucial details are spelled out fully (and omitted when reasonably obvious and less important). Going beyond merely proving some rather substantial theoretical results, the author then shows that the machinery he develops is also easily applicable, by showing that Savitch’s algorithm can be (naturally) expressed using a so-called rank-3 term, and thus showing that it recognizes only things in PSPACE.

The combined elegance of the results and the exposition is remarkable. The results also strike me as quite important. I have given this paper some of the highest praise I can: I have actively pointed it out to colleagues as a paper worth reading.