| 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.