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:

• 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.

Course material

• Course notes. (With hyperlinks into the Coq development.)
• The corresponding Coq development (pretty-printed).
• Raw Coq sources: Sem.v and Sequences.v
• The slides for the lecture.

Recommended reading

• Coq in a hurry, Yves Bertot.
• Winskel is (almost) Right: Towards a Mechanized Semantics Textbook, Tobias Nipkow.
• Coinductive big-step operational semantics, Hervé Grall and Xavier Leroy.

Coq pointers

• The Coq Web site: software and documentation.
• Interactive Theorem Proving and Program Development -- Coq'Art: The Calculus of Inductive Constructions, by Yves Bertot and Pierre Casteran: a comprehensive textbook on Coq.