Hacker News new | past | comments | ask | show | jobs | submit login

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.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact