Skip to content
Course website for CS6225 Prorgams and Proofs @ IITM Spring 2020 edition
Coq HTML Makefile CSS F* Ruby TeX
Branch: gh-pages
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
_css Initial commit Oct 13, 2019
_includes
_layouts Initial commit Oct 13, 2019
_posts Initial commit Oct 13, 2019
_sass Initial commit Oct 13, 2019
_tex
assets Initial commit Oct 13, 2019
assignments edits Jan 28, 2020
frap Added more lectures Dec 17, 2019
lectures Added PSet3 Jan 28, 2020
.gitignore Added more stuff Dec 17, 2019
Gemfile
Gemfile.lock Initial commit Oct 13, 2019
LICENSE
LICENSE.txt Initial commit Oct 13, 2019
README.md Update README.md Jan 22, 2020
_config.yml
assignments.md edits Jan 28, 2020
feed.xml Initial commit Oct 13, 2019
index.md Update time Jan 15, 2020
ipa.gemspec CS6XYZ -> CS6225 Nov 12, 2019
resources.md
schedule.md Added PSet3 Jan 28, 2020
sitemap.xml Initial commit Oct 13, 2019

README.md

CS6225 : Programs and Proofs

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.

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. 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
$ make

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

You can’t perform that action at this time.