Textbooks
PL Resources
Coq Resources

Coq resources

Coq is a formal proof management system in that a proof in the Coq programming environment is mechanically checked by the machine. It is based on the calculus of constructions (CoC), a higher-order typed lambda calculus initially developed by Thierry Coquand. Most of the resources below are derived from the main Coq page.

Fun example from Coq tutorial

A private club has the following rules:

1. Every non-scottish member wears red socks
2. Every member wears a kilt or doesn't wear red socks
3. The married members don't go out on Sunday
4. A member goes out on Sunday if and only if he is Scottish
5. Every member who wears a kilt is Scottish and married
6. Every scottish member wears a kilt

Coq < Check NoMember.
NoMember
  : forall Scottish RedSocks WearKilt Married GoOutSunday : Prop,
    (~ Scottish -> RedSocks) ->
    WearKilt \/ ~ RedSocks ->
    (Married -> ~ GoOutSunday) ->
    (GoOutSunday <-> Scottish) ->
    (WearKilt -> Scottish /\ Married) ->
    (Scottish -> WearKilt) -> False

Getting started

• Download Coq. You may find more detailed installation instruction on the POPLMark wiki here. Unless you have great desire to hand compile the binaries, downloading precompiled binaries should suffice. Instructions for the latter below:
  • Linux. Download the appropriate files based on your system. You will need glibc-2.4 to be able to run everything--you may need to upgrade your Linux distribution. (You may check what version you have with the command "ls -l /lib/libc-*".) You can download:
    • Files. Download the tar file, untar, and install.
    • RPM packages. Download the Coq and CoqIde RPM packages. Use an appropriate RPM package manager (alien with "alien -i [package name]" on Debian) to install.
  • Windows. Download coq-8.1pl3-1-win.exe from the link above and everything will install automatically.
  • Mac. There is an older version available on the website.
• Look through the Coq tutorial. (If the first tutorial did not please you, you may quickly get up to speed with Coq in a Hurry, another tutorial.) You can run Coq either from the terminal (with the command "coqc") or with the IDE (with the command "coqide"). The terminal will suffice for going through the tutorial.
• You may also find it useful to peruse the Coq Standard Library to see how Coq is used to build up logical and mathematical foundations.

• The reference manual, though not meant to be read end to end, has useful information for the use of Coq.
• Visit Cocorico!, the Coq wiki.
• Find example programs people have created here. To use the Makefile, you will need to have an Ocaml compiler installed.
• People have found it useful to use Proof General, a generic front-end for theorem provers based on Emacs. Tips:
  • The download links for Version 3.7 aren't ready yet, but the pre-release is available on the site. You can build the file archive yourself or use the RPM packages. Click here for a Windows tool for managing such files.
  • Click here for the Proof General Manual. It will walk you through installation and running with basic proofs.