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:

- Non-optimizing compilation of a structured imperative language to a virtual machine, and its correctness proof.
- Notions of semantic preservation.
- A panorama of mechanized semantics: small-step, big-step, coinductive big-step, definitional interpreter, denotational semantics.
- Examples of program optimizations: dead code elimination, register allocation.
- Design and soundness proof of a generic static analyzer based on abstract interpretation.
- Compiler verification "in the large" : an overview of the CompCert verified C compiler.

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

- The slides for the lecture: for presentation and for printing (6 on a page).
- Coq development, source distribution:
`compiler-verification.tar.gz`

.

(Includes a copy of "Software Foundations", for convenience). - Coq development, commented and pretty-printed for online viewing:
- Semantics: various forms of semantics for IMP.
- Compil: compilation from IMP to a virtual machine, big-step proofs of correctness.
- Compil_smallstep: same, with a small-step correctness proof.
- Deadcode: liveness analysis and dead code optimization.
- Regalloc: extension to register allocation.
- Analyzer1: a simple generic static analyzer based on abstract interpretation.
- Analyzer2: a more sophisticated version of the generic static analyzer.
- Library Sequences: transition sequences and their properties.
- Appendix Coinduction: inductive and coinductive definitions illustrated on an example.
- Appendix Fixpoint: computing fixpoints in well-founded lattices, with applications to liveness analysis.

- Xavier Leroy. Formal verification of a realistic compiler, Comm. ACM 52(7):107-115, 2009.

- Benjamin Pierce et al. Software Foundations.
- Hervé Grall and Xavier Leroy. Coinductive big-step operational semantics.
- Tobias Nipkow. Winskel is (almost) Right: Towards a Mechanized Semantics Textbook.
- Yves Bertot. Structural abstract interpretation, A formal study using Coq.
- Patrick Cousot. MIT Course 16.399: Abstract Interpretation.

- The Coq Web site: software and documentation.
- Coq in a hurry, Yves Bertot.
- Interactive Theorem Proving and Program Development -- Coq'Art: The Calculus of Inductive Constructions, by Yves Bertot and Pierre Casteran: a comprehensive textbook on Coq.

Xavier.Leroy@inria.fr