Lambda the Ultimate

Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy has written Formal verification of a C-Compiler frontend. Some previous work is already mentioned on LtU here. Abstract:

This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source and target languages as well as the translation between them have been written in the speci- fication language of the Coq proof assistant. The proof of observational semantic equivalence between the source and generated code has been machine-checked using Coq. An executable compiler was obtained by automatic extraction of executable Caml code from the Coq specification of the translator, combined with a certified compiler back-end generating PowerPC assembly code from Cminor, described in previous work.