3 Resources
Before coming to class, students should install the following software:
We recommend beginning by installing OPAM. This will allow you to create a sandboxed installation of OCaml. Please install OCaml version 4.12.0. The directions for installing Coq through OPAM can be found here: https://coq.inria.fr/opam-using.html.
For development, we strongly encourage students to use Emacs with the Proof General plugin. If you choose to do so, please install Proof General using the built-in package manager inside Emacs. This is described on the Proof General website linked above. DO NOT install it using your system’s package manager.
If you are uncomfortable using Emacs, you can alternatively install CoqIDE through OPAM.
Windows users may need to perform some extra configuration, described here: https://lemonidas.github.io/CoqWSL.html.
A cloneable .emacs startup config can be found here.
This course will use three volumes of the Software Foundations series:
Required Text
Benjamin C. Pierce, et al. Logical Foundations.
Benjamin C. Pierce, et al. Programming Language Foundations.
Leonidas Lampropoulos and Benjamin C. Pierce QuickChick: Property-Based Testing in Coq.
You are not required to purchase a physical copy of these texts. They can be browsed at the link above. Please don’t take Coq files (the .v source files) from the texts above, but rather download them from this website. We will be making modifications to SF as the semester goes on.
Installing QuickChick
You can install QuickChick through OPAM, using the following commands.
# Add the Coq opam repository (if you haven't already) |
opam repo add coq-released https://coq.inria.fr/opam/released |
opam update |
# Install the coq-quickchick opam package |
opam install coq-quickchick |
Further Reading
Benjamin C. Pierce. Types and Programming Languages.
Adam Chlipala. Certified Programming with Dependent Types (CPDT).
Using Coq
We will be using Coq 8.13.2 for the duration of this course.
Tactic cheat sheet (thanks to Arthur Azevedo de Amorim and Robert Rand)
- Proof General, and documentation. Useful key bindings (’C-x’ means Control/Command plus x):
C-c C-RET : Processes (or reverts) to the cursor
C-c C-n : Processes the next definition/element
C-c C-u : Undoes processing of the last element
C-c C-BS : Undoes and deletes the last element
C-c C-b : Processes the entire buffer
C-c C-r : Reverts all processing so far
C-C C-. : Enables "electric period" (or disables it) – immediately processes up to . when entered.
C-c C-a C-a : Search command
C-c C-a C-c : Check command
C-c C-a C-p : Print command
C-c C-; : Paste results of last Search command