The Coq proof assistant is the specific proof assistant that we will present in this lecture. It provides mechanisms for writing specifications, for developing interactively new proofs, and for checking existing proofs in batch mode. The user can reuse previously developed proofs and specifications. And finally it can extract proofs from programmes. It was developed at INRIA in France by several researchers starting from the first works by Huet and Coquand, and then by Paulin Mohring, Dowek, Werner and others.

---