This is the website for the Spring 2020 course "Programs and Proofs" at the Department of Computer Science and Engineering at the Indian Institute of Technology, Madras.
The lecture materials are available in lectures/. In order to step through the
lectures in CoqIDE, you will first need to build the Frap library in frap/. To
build, ensure that you have a Coq distribution installed. If you are using
CoqIDE ensure that there aren't two different distributions of Coq installed on
your machine. Easiest is to install the CoqIDE and then add the bin directory
from the distribution to your PATH. On MacOS, this means that the following
line is included in my .bashrc file:
export PATH=$PATH:/Applications/CoqIDE_8.10.2.app/Contents/Resources/bin/Now the frap library can be built by:
$ cd frap
$ makeThen you can open the *.v files in CoqIDE and step through.