This course website, including all of the lecture materials, lives here.
You will need to ensure that the location of the Coq binaries is in your
so that the make files for the frap book and the assignments work. On MacOS,
this means that the following line is included in my
This will vary between OS versions. We will ensure that everyone has a working environment by the end of first week.
We will be closely following
- Formal Reasoning about Programs, Adam Chlipala. Freely available online.
Other reference books are:
- Software Foundations, Benjamin Pierce et al. Freely available online.
- Types and Programming Languages, Benjamin Pierce, MIT Press, 1st edition,
- Ebook is available in IITM library.
- Practical Foundations for Programming Languages, Robert Harper, Cambridge University Press, 2nd edition, 2016. Freely available online.