with applications to program proof and compiler verification
The goal of this lecture is to show how modern theorem provers --
I use the Coq proof assistant -- can be used to mechanize the
specification of programming languages and their semantics, and to
reason over individual programs as well as over generic program
transformations, as typically found in compilers.
The topics covered include:
- Operational semantics: small-step, big-step, definitional interpreters.
- Some forms of denotational semantics.
- Axiomatic semantics and Hoare logic.
- Generation of verification conditions; application to program proof.
- Compilation to virtual machine code and its proof of correctness.
- An example of an optimizing program transformation and its proof of correctness.