Abstracting Abstract Machines (2010) [pdf]

This is a beautiful paper that anyone interested in abstract interpretation and sound static analysis probably already knows, but the core idea is quite accessible.

An abstract machine is a formalization of the concrete semantics of a programming language, and we'd like to be able to "lift" that concrete semantics to an abstract semantics: a finite (and therefore computable) over-approximation of program semantics.

However, the concrete structures of an abstract machine (most notably continuations) are themselves potentially infinite, so you can't just build a "structural abstraction" by applying the abstraction function pointwise over concrete structures -- the resulting abstraction is infinite and thus static analysis may diverge.

That's where this paper comes in: its key insight is that, by store-allocating continuations and bounding the number of store addresses, you can finitize an abstract machine such that structural abstraction works out nicely while preserving the underlying semantics.

I posted this because just this week it won the ICFP Most Influential Paper Award: https://www.umiacs.umd.edu/about-us/news/van-horn-wins-most-...

This paper won the Most Influential Paper Award just yesterday at ICFP'2020.

Award video: https://www.youtube.com/watch?v=WfRqE4NBecM