Oregon Programming Languages Summer School 2012

Proving a Compiler:

Mechanized verification of program transformations and static analyses

(The 2011 edition of this lecture is also available, with different contents.)


Formal semantics of programming languages supports not only reasoning over individual programs (program correctness), but also reasoning over program transformations and static analyses, as typically found in compilers (tool correctness). With the help of a proof assistant, we can prove semantic preservation properties of program transformations and semantic soundness properties of static analyses that greatly increase the confidence we can have in compilers and program verification tools.

The topics covered in this lecture include:

We will use the Coq proof assistant and build on the formalization of the IMP language shown in Benjamin Pierce's "Software Foundations" lectures.

Course material

Introductory reading

Further reading

Coq pointers