Abstract interpretation is an important conceptual framework that unifies many different concepts in static analysis. However, writing a general, modular, abstract interpreter has not been as straightforward. There are two difficulties: a software engineering challenge, and an encoding issue. The software engineering challenge is to find the right abstractions that capture the kind of polymorphism inherent in abstract interpretation. The encoding issue involves finding a way to phrase the operational semantics of languages using a suitable abstract machine that lends itself well to abstract interpretation.

This is exactly what the authors solve in this gem of a paper. Aimed directly at experts, the paper walks readers through the process of taking a lambda calculus and rewriting it (using continuation passing style, an explicit store, and explicit contexts) so that it is better suited for abstract interpretation. Next, using an explicit implementation in Haskell, various aspects (nondeterminism, store, time, and addresses) are systematically abstracted away from the interpreter into a monad.

Then, to prove that this beautiful series of abstractions is more than mere theory, the authors show how to concretely implement a variety of analyses using this framework. While this section might seem a little ad hoc, they then show how it all fits together in an elegant conceptual framework.

This paper is a real tour de force. Not only is it very well written, it presents an extremely elegant solution to an important, thorny problem. The only unfortunate aspect is that the authors chose an initial algebra encoding of their base language, rather than the much more flexible “finally tagless” encoding.