CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote)

Abstract

A formally verified compiler ensures that compilation does not introduce any bugs in programs. In the CompCert C compiler, this correctness property requires reasoning about realistic languages by using a semantic framework. This invited talk explains how this framework has been effectively used to turn CompCert from a prototype in a lab into a real-world compiler.