Lambda the Ultimate

I mentioned this somewhat passingly a few years ago. So not to make the same mistake again, I'm reposting this as a top-level post (and with current links).

His list of publications and the recent ones. Some relatively recent work by him discussed on LtU is here.

The ones I want to highlight in particular are his applications of the Curry-Howard correspondence to machine code generation and such topics.

Lifting Abstract Interpreters to Quantified Logical Domains. Sumit Gulwani, Bill McCloskey, Ashish Tiwari. July 2007.

Today, abstract interpretation is capable of inferring a wide variety of quantifier-free program invariants. In this paper, we describe a general technique for building powerful quantified abstract domains that leverage existing quantifier-free domains. For example, from a domain that abstracts facts like "a[1] = 0", we automatically construct a domain that can represent universally quantified facts like "Forall i: (0 <= i < n) => A[i]=0)". The principal challenge in building such a domain is that, while most domains supply over-approximations of operations like join, meet, and variable elimination, working with the guards of quantified facts requires under-approximation...

Using our generic construction, we build a number of abstract interpreters on top of domains for linear arithmetic, uninterpreted function symbols (used to model heap accesses), and pointer reachability. Our experiments on a variety of programs using arrays and pointers (including several sorting algorithms) demonstrate the feasibility of the approach on challenging examples.

Escape from Zurg: An Exercise in Logic Programming by Martin Erwig. Journal of Functional Programming, Vol. 14, No. 3, 253-261, 2004

In this article we will illustrate with an example that modern functional programming languages like Haskell can be used effectively for programming search problems, in contrast to the widespread belief that Prolog is much better suited for tasks like these.

...

The example that we want to consider is a homework problem that we have given in a graduate level course on programming languages. The problem was one of several exercises to practice programming in Prolog. After observing that many students had problems manipulating term structures in Prolog (after already having learned to use data types in Haskell) and spending a lot of time on debugging, the question arose whether it would be as difficult to develop a solution for this problem in Haskell. This programming exercise worked well, and we report the result in this paper.

(Haskell source code)