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)