A Short Course on Interactive Proofs in Coq/Ssreflect

This project contains the Coq sources, the lectures and the exercises for the course

"Programs and Proofs: Mechanizing Mathematics with Dependent Types".

The latest draft of the accompanying lecture notes can be downloaded from the official course page:

http://ilyasergey.net/pnp

Initial release: August 2014

Building the project and the lecture notes

Just run make. This will compile all lecture files, solutions and create the file latex/pnp.pdf with lecture notes.