Program Proving
Documentation
Yves Bertot's home page
Yves Bertot is a researcher at Inria, and co-author of the Coq'Art book , wrote a lot of tutorials on Coq and its main applications in mathematics and computer science. Please click
here !
Coq sources (under construction)