3 Resources
Before coming to class, students should install the following software:
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.8.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-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-; : Paste results of last Search command