Mechanized semantics, with applications to program proof and compiler verification, lecture given at the 2009 Marktoberdorf summer school

Abstract. The goal of this lecture is to show how modern theorem provers—in this case, the Coq proof assistant—can be used to mech-anize the specification of programming languages and their semantics, and to reason over individual programs and over generic program trans-formations, as typically found in compilers. The topics covered include: operational semantics (small-step, big-step, definitional interpreters); a simple form of denotational semantics; axiomatic semantics and Hoare logic; generation of verification conditions, with application to program proof; compilation to virtual machine code and its proof of correctness; an example of an optimizing program transformation (dead code elimi-nation) and its proof of correctness