Coq for Programming Language Metatheory

A course at the Summer School on Logic and Theorem Proving in Programming Languages, Eugene, Oregon, July 2008

Overview

The speakers will present a hands-on tutorial on the use of the Coq proof assistant in formalizing programming language metatheory. The tutorial is tailored to people who are familiar with syntactic proofs of programming language metatheory, such as type soundness, but have never used a proof assistant to create and check such proofs. At the end, participants will have a reading knowledge of Coq and a running start on using Coq in their own work. The tutorial is composed of two pieces: a basic introduction to defining language semantics in Coq as well as the proof of simple results, as well as a more specialized treatment of the representation of binding structures. Both parts include interactive demos and exercises.

Required software

The Coq Proof Assistant, version 8.1pl3.

• Make sure you have a working copy of CoqIDE or ProofGeneral.
• Earlier 8.1 releases may work but are untested.
• The code is known not to work with version 8.2 due to significant changes in Coq's standard library.
• It should not matter whether you install a binary package or compile Coq from source. In addition to the resources available through Coq's homepage, the POPLmark wiki also contains some tips on installing Coq.

The Coq code for this tutorial.

• Last updated: 2007-07-25.
• Download: coq-tutorial.zip
• Start with the README file provided in the zip file.