Today's lecture will deal with a specific proof assistant whose name is Coq. A proof assistant is a tool, a computer programme that will assist the user to specify theorems and programmes and to build actual proofs of those theorems. Or programmes satisfying those specifications. We will first treat the problem of what it means to have a computer aided formal reasoning, and then we will give some details about Coq, its specification language first and then its proof system. More advanced topics will have to be left to more specific lectures, for instance the calculus of co-inductive constructions, the utilities that come with the system Coq, the proof extraction procedure and finally Coq as a logical framework.

---