3 Resources
Before coming to class, students should install the following software:
A handy guide to install these in Windows through opam is available here.
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 downloaded from the link above, and the source for the texts (a series of .v Coq source files) will be used for problem sets.
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.12 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