Compiler correctness proofs

Question

I am looking for tutorial material that covers compiler correctness proofs, preferably using denotational methods, at the level of a beginning grad student.

Alternatively, do you know of some simple compiler examples that I could use to illustrate the issues? (The first example that occurred to me was a translator from infix to postfix expressions. But it failed to show anything interesting other than how to do induction on syntax.)

Answer 1

I do not know of good tutorial material, but there are papers that are sufficiently elementary for a grad student (like me). The first might be what you are looking for (emphasis is mine).

Simple relational correctness proofs for static analyses and program transformations, Nick Benton. 2004.

We show how some classical static analyses for imperative programs, and the optimizing transformations which they enable, may be expressed and proved correct using elementary logical and denotational techniques. The key ingredients are an interpretation of program properties as relations, rather than predicates, and a realization that although many program analyses are traditionally formulated in very intensional terms, the associated transformations are actually enabled by more liberal extensional properties.

These papers may also interest you. They helped me greatly!

1. Proving Correctness of Compiler Optimizations by Temporal Logic, David Lacey, Neil D. Jones, Eric Van Wyk, Carl Christian Frederiksen. I would have thought there was more material using bisimulation in the context of compiler optimizations. If your aim is really denotational techniques, you can probably encode these proofs using characterisations of bisimulation.
2. Generating Compiler Optimizations from Proofs, Ross Tate, Michael Stepp, and Sorin Lerner. Includes a category theoretic formalisation of their proof method.
3. Proving Optimizations Correct using Parameterized Program Equivalence, Sudipta Kundu, Zachary Tatlock, and Sorin Lerner. Go there if you like logical relations.
4. A Formally Verified Compiler Back-end Xavier Leroy.

Answer 2

You'll need to modernize the notation, but McCarthy and Painter's Correctness of a Compiler for Arithmetic Expressions is simple and good, and also of historical interest (since to the best of my knowledge it's the first paper on the subject).

Answer 3

Adam Chlipala's A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language seems to be a good example of a simple compiler correctness proof using denotational methods, with the added advantage of having been formalized completely in a proof assistant.

Answer 4

Graham Hutton has a small example in his book "Programming in Haskell" which is a great place to start.

I also have a few mechanised proofs (various logics) of the McCarthy-Painter compiler in a report I did for my PhD.

Answer 5

Perhaps not the simplest example, but Xavier Leroy has done a lot of work in this area, such as a formally verified C compiler. He gave a summer school presentation using a small imperative language IMP, which is an accessible introduction to the more advanced work.