• Cours multimédia Coq (Yves Bertot), les diapos 1 2 3 4 5 6 7 8
• Mini Guide Coq rédigé par Christine Paulin
• Quelques tactiques de Coq, PDF (Joe Redmon)

Documents rédigés par Christine Tasson

1. Cours Coq
2. TP1 : énoncé, squelette
3. TP1bis : squelette
4. TP2 : énoncé, squelette
   Extraire le code OCaml via la commande Coq Recursive Extraction mult.
   Copier le code dans Try OCaml et tester.
5. TP2bis : énoncé, squelette (Christine Paulin)
6. TP2ter : squelette
   Exemples pour tester le code OCaml :

   search O Empty
   search O (Node(Empty, O, Empty)) 
   search O (Node(Empty, (S O), Empty)) 
   search O (Node(Node(Empty,O,Empty), (S O), Empty))
   search O (Node(Empty, (S O), Node(Empty, O, Empty)))

7. TP3 : énoncé, squelette
8. TP4 : énoncé
9. TP5 : énoncé, squelette