Tutorial Materials for Programming Language Research

Getting started: You will need the following software.

  • Coq: Version 8.1 or a later release. Binary and source packages are available from the Coq homepage.
  • Either CoqIDE (comes with Coq) or Proof General. Both provide interactive environments for developing proofs and are easier to work with than Coq's toploop.
  • coq-tutorial.zip, which contains all the Coq files and documentation for this tutorial. The remainder of this page is dedicated to describing the contents of this zip-file and providing easy-to-browse HTML versions of the Coq code; you do not need to download anything else. The README.txt file explains how to compile our library for programming language metatheory. You should compile this library before proceeding further.

Introduction to Coq

The file CoqIntro.v is a self-contained introduction to Coq, with a number of examples and exercises demonstrating Coq's basic facilities. The file is designed to be worked through interactively. (Note that you should work through the .v file that came with the .zip file you downloaded. The HTML version linked to above is there in case you want an easy to browser version of the file.) Solutions to exercises are at the end of the file.

The simply-typed lambda calculus

The file STLC_Tutorial.v is a formalization of the simply-typed lambda calculus. Like CoqIntro.v, this file contains a number of examples and exercises, and is designed to be worked through interactively. (As before, you should work through the .v file that came with the .zip file, not the HTML version linked above.) Solutions to the exercises are in STLC_Solutions.v.

This part of the tutorial relies on a library for programming language metatheory that we have developed. Working through STLC_Tutorial.v introduces this library as it is used in practice.

System F<:

The final portion of this tutorial is to extend our formalization of type safety for System F<: (Fsub) to include sum types and let expressions. This development consists of four files: Fsub_Definitions.v, Fsub_Infrastructure.v, Fsub_Lemmas.v, and Fsub_Soundness.v.

In order to get a handle on this relatively large development, you may want to first look through its four files using the links above. They're organized so that related definitions and lemmas are placed in the same file. A few additional points that were not covered in STLC_Tutorial.v are listed below.

  • The later files in this development load the earlier ones using Require Export lines near the beginning of the files. (You can read more about this command in the Coq Reference Manual.) For example, the "infrastructure" file loads the "definitions" file.
  • Require Export loads a compiled version of the file given to it, not the original source file. To compile, e.g., Fsub_Definitions.v, run coqc Fsub_Definitions.v. This creates a file Fsub_Definitions.vo, which is a compiled version of the .v file. Whenever you change a file that is loaded by another, you should recompile it. (Note that Coq will not warn you if a .v file is newer than the corresponding .vo file.)
  • The development uses substantial amounts of automation to make the proofs tractable. Every file except Fsub_Soundness.v ends with a block of hints for Coq's auto and eauto tactics, and a brief discussion of what those hints accomplish.
  • The proof of typing_through_subst_ee is heavily commented, since it illustrates several tactics for working with environments. (The comments will make more sense if you are interactively stepping through the proof.) These tactics were skipped over in STLC_Tutorial.v.

Our solution: The files Fsub_LetSum_*.v contain our solution. The one non-obvious (and non-necessary) difference is the definition of a new unary predicate body_e, which is used in the definition of the reduction and associated infrastructure lemmas.