Semantics

We will be using the Coq proof assistant to formally check our results during this course. We are assuming you are familiar with the basic usage of Coq (for instance, as taught in the Introduction to Computational Logic Course at Saarland University, the particular iteration (e.g., 2021 or earlier) of the course does not matter).

Since we will be using a number of libraries throughout the course (and to prevent incompatibilities with different Coq versions), we are assuming that you are using opam for managing your Coq installations. opam is readily available for Linux and macOS, but sadly not for Windows. Windows users can use a VM we provide (see the Materials page). A setup via WSL or Cygwin is also possible, but we do not provide support for that.

You can find instructions for setting up Coq in the right way here.

We publish the Coq development for the course gradually as the course goes on via our Gitlab repository.