Software Foundations in Coq

This page contains useful materials for the Coq Boot Camp and lectures on Software Foundations in Coq.

Hints on Using Coq for OPLSS 2013

These notes are intended to help you get a working and useful version of Coq 8.4 running on your laptop or other personal machine prior to the boot camp.

If you find errors here or have suggestions that might be useful for others, let me know (by mail to apt@cs.pdx.edu) and I'll update this page.

What you'll need

A working Coq installation contains several pieces:

Choosing an IDE

To use Coq effectively, you must have a working IDE for it. There are two in common use: Both of these IDE's work by running a coqtop process in the background, so this must be installed successfully in any case.

Coq Installation

Most of the required pieces can be obtained from the official Coq Download page. The most recent stable release of Coq is version 8.4pl2. For the version of the Software Foundations textbook we will use, any variant of Coq version 8.4 should work (but Windows/CoqIDE users see note below). Versions below 8.4 will not work.

Proof General can be downloaded from here; you should use the most recent stable version, which is 4.2.

Some platform-specific notes on installation follow:

IDE Configuration

Although both CoqIDE and PG come with lots of fancy features, you really only need support for four commands: It is essential that at least the first three of these commands be bound to keyboard shortcuts, as you will use them constantly when working on Coq script files. While both IDE's support such shortcuts, they can be tricky to get right on Macs and (for CoqIDE) on some linux window managers. CoqIDE users should plan on needing to edit their .coqide.keys file directly, as described in the documentation; this page may also be useful.

Other points:

Suggested Exercises

Exercises worked during the boot camp or suggested as especially good homework targets: