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

Using Coq

We will be using Coq 8.17.1 for the duration of this course.