Planning des cours
| Date | Titre width=30% | Transparents | Exercices | A faire | |
|---|---|---|---|---|---|
| Séance 1 | 04/10/2006 | Systèmes de déduction et initiation à Coq | cours1.pdf | prop.v pred.v | Lire intro, chap 1 et chap 4 de Introduction to proof theory par Gilles Dowek |
| Séance 2 | 18/10/2006 | Types de données inductifs et prédicats inductifs. Les types inductifs en Coq | cours2.pdf | arithmetique.v append.v sort.v | Lire (partiellement) les chap 6 et chap 8 du Coq'Art Projets individuelles à rendre avant le vendredi 1er Décembre |
| Séance 3 | 08/11/2006 | Typage | cours3.pdf | ||
| Séance 4 | 22/11/2006 | Programmation certifiée avancée | cours4.pdf | minus.v set.v | Finir l'exercice sur les ensembles finis |
| Séance 5 | 06/12/2006 | Logique équationnelle et réécriture | newman_exo.v cours5_exo.v | ||
| Séance 6 | 20/12/2006 | Arithmétique et procédures de décision | cours6.pdf | pieces_exo.v reflexive_exo.v cours6.v |
Lieu : Salle Noirmoutier
Horaire : 14h - 17h
Liens
- Le manuel d'utilisation de Coq
- Une introduction rapide à Emacs
- Un livre sur Coq : Interactive Theorem Proving and Program Development. Coq'Art : the Calculus of Inductive Constructions par Yves Bertot et Pierre Casteran, Springer-Verlag
Installer Coq chez soi
- Installer la dernière version de Coq
- Décompresser le repertoire ProofGeneral chez vous
- Ajouter le contenu de ce fichier à votre fichier .emacs en adaptant la ligne (load-file "~/soft/src/ProofGeneral/generic/proof-site.el") avec le bon chemin d'accès à votre répertoire ProofGeneral.
Me contacter en cas de problème