Verification Technology, Systems & Applications summer school 2013

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.
• Software Foundations by Benjamin C. Pierce et al.