2 Resources
Required Text
Benjamin C. Pierce, et al. Logical Foundations.
Benjamin C. Pierce, et al. Programming Language Foundations.
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.
Recommended Texts
Adam Chlipala. Certified Programming with Dependent Types (CPDT).
Anders Møller and Michael I. Schwartzbach. Static Program Analysis.
Robert Harper. Practical Foundations for Programming Languages.
Benjamin C. Pierce. Types and Programming Languages.
Using Coq
We will be using Coq 8.6 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