<p>You'll need to modernize the notation, but McCarthy and Painter's <a href="http://www-formal.stanford.edu/jmc/mcpain.ps"><em>Correctness of a Compiler for Arithmetic Expressions</em></a> is simple and good, and also of historical interest (since to the best of my knowledge it's the first paper on the subject). </p>

CC BY-SA 3.0
2012-03-06T09:52:00.077Z
2012-03-06T09:52:00.077Z
Neel Krishnaswami
<p>Adam Chlipala's <a href="http://adam.chlipala.net/papers/CtpcPLDI07/CtpcPLDI07.pdf">A Certified Type-Preserving Compiler from Lambda Calculus to
Assembly Language</a> 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.</p>

CC BY-SA 3.0
2012-03-06T20:50:35.570Z
That's a very good paper.
Neel Krishnaswami
CC BY-SA 3.0
2012-03-06T10:54:30.197Z
2012-03-06T10:54:30.197Z
cody
<p>Perhaps not the simplest example, but Xavier Leroy has done a lot of work in this area, such as <a href="http://compcert.inria.fr/">a formally verified C compiler</a>. He gave a <a href="http://gallium.inria.fr/~xleroy/courses/Eugene-2011/">summer school presentation</a> using a small imperative language IMP, which is an accessible introduction to the more advanced work.</p>

CC BY-SA 3.0
2012-03-06T15:40:41.103Z
2012-03-06T15:40:41.103Z
Dave Clarke
<p>Graham Hutton has a small example in his book <a href="http://www.cs.nott.ac.uk/~gmh/book.html">"Programming in Haskell"</a> which is a great place to start.</p>

<p>I also have a few mechanised proofs (various logics) of the McCarthy-Painter compiler in a <a href="http://www.cs.york.ac.uk/fp/jason-docs/ReichPR2011.pdf">report I did for my PhD</a>.</p>

CC BY-SA 3.0
2012-03-06T10:58:38.260Z
2012-03-06T10:58:38.260Z
Jason Reich
<p>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).</p>

<blockquote>
  <p><a href="http://dl.acm.org/citation.cfm?id=964001.964003"><em>Simple relational correctness proofs for static analyses and program transformations</em></a>, Nick Benton. 2004.</p>
  
  <p>We show how some classical static analyses for imperative programs, and the optimizing transformations which they enable, may be expressed and <em>proved correct using elementary logical and denotational techniques</em>. 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.</p>
</blockquote>

<p>These papers may also interest you. They helped me greatly!</p>

<ol>
<li><a href="http://www.dcs.warwick.ac.uk/people/academic/David.Lacey/papers/proving.pdf">Proving Correctness of Compiler Optimizations by Temporal Logic</a>, 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.</li>
<li><a href="http://cseweb.ucsd.edu/~lerner/papers/popl10.html">Generating Compiler Optimizations from Proofs</a>, Ross Tate, Michael Stepp, and Sorin Lerner. Includes a category theoretic formalisation of their proof method.</li>
<li><a href="http://dl.acm.org/citation.cfm?id=1542513">Proving Optimizations Correct using Parameterized Program Equivalence</a>, Sudipta Kundu, Zachary Tatlock, and Sorin Lerner. Go there if you like logical relations.</li>
<li><a href="http://www.springerlink.com/content/n513653k294m871k/">A Formally Verified Compiler Back-end</a> Xavier Leroy.</li>
</ol>

CC BY-SA 3.0
2012-03-07T07:10:50.420Z
2012-03-07T07:10:50.420Z
Vijay D
<p>I am looking for tutorial material that covers compiler correctness proofs, preferably using denotational methods, at the level of a beginning grad student.  </p>

<p>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.)</p>

<reference-request><pl.programming-languages><semantics><compilers>
Compiler correctness proofs
Uday Reddy
# Compiler correctness proofs

(Asked by: username_0 on 2012-03-06)

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.)

**Tags:** reference-request, pl.programming-languages, semantics, compilers

---

## 5 answers

### Answer by username_5 on 2012-03-07. Score: 11 | Accepted answer

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*](http://dl.acm.org/citation.cfm?id=964001.964003), 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](http://www.dcs.warwick.ac.uk/people/academic/David.Lacey/papers/proving.pdf), 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](http://cseweb.ucsd.edu/~lerner/papers/popl10.html), Ross Tate, Michael Stepp, and Sorin Lerner. Includes a category theoretic formalisation of their proof method.
3. [Proving Optimizations Correct using Parameterized Program Equivalence](http://dl.acm.org/citation.cfm?id=1542513), Sudipta Kundu, Zachary Tatlock, and Sorin Lerner. Go there if you like logical relations.
4. [A Formally Verified Compiler Back-end](http://www.springerlink.com/content/n513653k294m871k/) Xavier Leroy.


---

### Answer by username_1 on 2012-03-06. Score: 10

You'll need to modernize the notation, but McCarthy and Painter's [*Correctness of a Compiler for Arithmetic Expressions*](http://www-formal.stanford.edu/jmc/mcpain.ps) 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 by username_2 on 2012-03-06. Score: 7

Adam Chlipala's [A Certified Type-Preserving Compiler from Lambda Calculus to
Assembly Language](http://adam.chlipala.net/papers/CtpcPLDI07/CtpcPLDI07.pdf) 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.

> **Comments:**
> **username_1**: That's a very good paper.  

---

### Answer by username_3 on 2012-03-06. Score: 7

Perhaps not the simplest example, but Xavier Leroy has done a lot of work in this area, such as [a formally verified C compiler](http://compcert.inria.fr/). He gave a [summer school presentation](http://gallium.inria.fr/~xleroy/courses/Eugene-2011/) using a small imperative language IMP, which is an accessible introduction to the more advanced work.


---

### Answer by username_4 on 2012-03-06. Score: 7

Graham Hutton has a small example in his book ["Programming in Haskell"](http://www.cs.nott.ac.uk/~gmh/book.html) 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](http://www.cs.york.ac.uk/fp/jason-docs/ReichPR2011.pdf).


---

