Using Proof Assistants for Programming Language Research or,
How to write your next POPL paper in Coq

San Francisco, CA

January 8th, 2008

A tutorial on the use of the Coq proof assistant in formalizing programming language metatheory.

This tutorial will be 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 of the session, participants will have a reading knowledge of Coq and a running start on using Coq in their own work.

This tutorial will be hands-on; participants are strongly encouraged to bring a laptop running Coq 8.1 (or a later release) and either Proof General or CoqIDE. The POPLmark wiki has instructions for installing Coq and Proof General.

Registration for the tutorial is online, through the POPL 2008 website.

Topics

• Defining language semantics in Coq
  • Abstract syntax
  • Inductively-defined relations
  • Derivations
• Proving simple results
  • Fundamental tactics
  • Automation
  • Forward and backward reasoning
• Scaling up to POPLmark
  • Semantic functions and conversion
  • Sets and environments
• Representing binding
  • Locally nameless representation
  • Freshness through cofinite quantification
  • Syntactic type soundness

Materials

The Coq code and documentation for this tutorial is available online. If you are attending the tutorial, we encourage you to download these materials and compile them beforehand. If you are not attending, these materials are self contained; you are welcome and encouraged to step through them on your own.

Schedule

Location: Stanford Ballroom East

08:00 - 08:30: Breakfast
08:30 - 09:00: Set-up, help with installation
09:00 - 10:00: Session I
10:00 - 10:30: Break
10:30 - 12:00: Session II
12:00 - 13:30: Lunch
13:30 - 15:30: Session III
15:30 - 16:00: Break
16:00 - 17:00: Session IV