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

Using Coq

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