Marktoberdorf 2009 summer school

Mechanized semantics

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:

Course material

Recommended reading

Coq pointers