COQ

• Welcome
• Home
• Publications
• My tip and tricks
• (internal)

• My tools
• Certificate Translator
• Coq DpdGraph
• ocamlannot
• PHP calendar

• Bookmarks
• Static Analysis
• Coq
• Security
• Development
• Other links

Liens

• la page officielle,
• FAQ, et aussi Cocorico! le Wiki de Coq,
• Pour voir à quoi ça ressemble, et/ou rentrer rapidement dans le vif du sujet~:
  • Coq in a Hurry : d'Yves Berot ;
  • ou Petit guide de survie en Coq d'Alexandre Miquel ;
  • Un cours de Jean Dupras en 13 leçons que je trouve très clair ;
• Coq'Art : la page du livre sur Coq,
• un autre très bon cours : Software Foundations par Benjamin C. Pierce, introduit COQ en détail, et parle également de sémantique des programmes, etc.
• POPL'2008 tutorial : "How to write your next POPL paper in Coq"
• HELM : peut aider à trouver des choses dans les bibliothèques de coq (quand ça marche...)
• Langage de Preuves Déclaratif (C-zar)
• Cours MPRI
• Adam Chlipala utilise beaucoup Ltac et présente ces exprériences dans Certified Programming with Dependent Types. Ça serait intéressant de passer un peu de temps a étudier ça...
• A mes tout début de Coq, je me suis fait un petit aide mémoire qui a ensuite été amélioré par Clément Hurlin : quickref.pdf (quickref.tex)
• ProofWeb permet d'utiliser COQ sur le Web. Il contient également une série d'exercices...
• le Sudoku de Laurent : une applet java à partir d'un programme COQ...
• A explorer/tester un jour :
  • Tactics for Rewriting modulo associativity and commutativity