Lecture notes for a short course on proving/programming in Coq via SSReflect.
Coq TeX Makefile
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.


Programs and Proofs

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:


Initial release: August 2014

Building the Project



We recommend installing the requirements via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect

Then, run make clean; make from the root folder. This will compile all lecture files, solutions and create the file latex/pnp.pdf with lecture notes.