3 Resources

Before coming to class, students should install the following software:

We recommend beginning by installing OPAM. This will allow you to create a sandboxed installation of OCaml. Please install OCaml version 4.12.0. The directions for installing Coq through OPAM can be found here: https://coq.inria.fr/opam-using.html.

For development, we strongly encourage students to use Emacs with the Proof General plugin. If you choose to do so, please install Proof General using the built-in package manager inside Emacs. This is described on the Proof General website linked above. DO NOT install it using your system’s package manager.

If you are uncomfortable using Emacs, you can alternatively install CoqIDE through OPAM.

Windows users may need to perform some extra configuration, described here: https://lemonidas.github.io/CoqWSL.html.

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 browsed at the link above. Please don’t take Coq files (the .v source files) from the texts above, but rather download them from this website. We will be making modifications to SF as the semester goes on.

Installing QuickChick

You can install QuickChick through OPAM, using the following commands.

# Add the Coq opam repository (if you haven't already)

opam repo add coq-released https://coq.inria.fr/opam/released

opam update

# Install the coq-quickchick opam package

opam install coq-quickchick

Further Reading

Using Coq

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