3 Resources
While the course will be paper-driven, having the following software installed could help tinker with some of the ideas we will cover.
A handy guide to install some of these in Windows through opam is available here.
A cloneable .emacs startup config can be found here.
Further Reading for Verification component
Benjamin C. Pierce, et al. Software Foundations
Benjamin C. Pierce. Types and Programming Languages.
Adam Chlipala. Certified Programming with Dependent Types (CPDT).
For the Coq components:
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