CS6225 : Programs and Proofs

This is the website for the Spring 2025 course "Programs and Proofs" at the Department of Computer Science and Engineering at the Indian Institute of Technology, Madras.

Coq sources

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.

The frap library can be built by:

$ cd frap
$ make

Then you can open the *.v files in CoqIDE and step through.