Marktoberdorf 2009 summer school

Mechanized semantics

with applications to program proof and compiler verification

Abstract

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


Xavier.Leroy@inria.fr