Support de cours
Formation COQ 25-27 février 2002






1   Sources de Coq

Les sources de la version de Coq utilisée dans la formation.

2   Utilisation de Proof General

3   Documentation

La documentation Coq V7 au format HTML

4   Lundi 25 février

4.1   Cours

Copie des transparents

4.2   Exemple du damier

Le squelette de l'exemple du damier

La solution du damier-html(code source)

5   Mardi 26 février

5.1   Cours

Copie des transparents

5.2   Exemple en sémantique

Le squelette de l'exemple en sémantique

La solution de l'exemple en sémantique-html (code source)

Le squelette des définitions sur les relations

La solution de l'exemple sur les relations (code source)

La preuve de l'algorithme d'exclusion mutuelle (code source)

6   Mercredi 27 février

6.1   Cours

Copie des transparents

6.2   Preuve de programmes

Solution de l'exercice de certification de programmes-html (code source)

6.3   Tactique réflexive

Le squelette de l'exemple de tactique réflexive

La solution de l'exemple-html (code source)

7   Informations supplémentaires


This document was translated from LATEX by HEVEA.