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
- Coq, versions from 8.7 to 8.11.1
- Mathematical Components, versions from 1.6.2 to 1.10.0 (
ssreflect
package) - FCSL-PCM, versions 1.0.0, 1.1.0, or 1.2.0
- Hoare Type Theory
We recommend installing the requirements via opam:
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add coq-htt git+https://github.com/TyGuS/htt\#master --no-action --yes
opam install coq coq-mathcomp-ssreflect coq-fcsl-pcm coq-htt
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.