Formation à l'assistant de preuve COQ
Programme provisoire

25-27 février 2002






1   Lundi 25 février

Cette journée est consacrée à une introduction à l'assistant Coq. À la fin de la journée, les participants auront acquis une connaissance des fonctionnalités de l'outil, pourront comprendre un développement réalisé en Coq et développer eux-mêmes un exemple simple. Cette journée est accessible à tous.

9h30 : Introduction générale

Objectifs de la séance
vue d'ensemble de l'outil Coq
Durée
30 mn
Contenu
Présentation générale de Coq : architecture sûre, preuves explicites, domaine d'application. Liens avec PVS, HOL, B.
Formateur
C. Paulin

10h : Le langage de specification

Objectifs de la séance
Apprentissage du langage de spécification (Gallina)
Durée
1h de cours + 1h de TP
Contenu
Formalisme : Lambda-calcul typé, logique d'ordre supérieur, fonctions, définitions inductives.
Gallina : Variable/Definition/Inductive/Cases/Fixpoint
Coq : Require/Check/Eval/Search
Formateur
B. Werner
TP
Exemples simples : axiomatisation au premier ordre, relations, fonctions sur les entiers (nat et Z), définitions inductives de base (fermeture transitive).

14h : le langage de preuves

Objectifs de la séance
Initiation aux tactiques de base
Durée
45mn de cours + 45mn de TP
Contenu
Formalisme : tactiques, termes de preuve
Tactiques de base : Intro/Apply/Elim/Trivial/Simpl
Tactiques automatiques : Tauto/Auto/Omega
Combiner les tactiques : THEN, THENS, Try, Orelse
Formateur
B. Werner
TP
Exemples simples : logique propositionnelle preuve par récurrence, simplification

15h30 : Outils

Objectifs de la séance
améliorer l'efficacité du développement
Durée
30mn (Cours-TP)
Contenu
Version native/byte-code
Makefile, coqdoc
interfaces : Ctcoq / ProofGeneral
Recherche dans les bibliothèques (Search/SearchPattern)
Organisation de la documentation, pointeurs sur des documents associés
Formateur
C. Paulin

16h30 : Développer un exemple simple

Objectifs de la séance
expérimenter une modélisation et une preuve en Coq
Durée
1h (TP)
Contenu
Le damier de Cachan
Formateurs
C. Paulin & B. Werner

2   Mardi 26 février

Cette journée est l'occasion de présenter les particularités du langage de spécification de Coq. L'accent sera mis sur comment représenter une notion de manière fonctionnelle ou inductive. Cette journée est accessible aux personnes ayant déjà une expérience de développement dans Coq ou bien ayant suivi la première journée.

9h30 : Manipulations des définitions inductives

Objectifs de la séance
initier aux outils spécifiques associés aux definitions inductives

Durée
1h cours - 1h30 TD
Contenu
Conditions de positivité, sortes
Schémas d'éliminations (dépendance, élimination forte, Scheme)
Tactiques spécifiques (EqDecide/Inversion/Discriminate)
Récursion structurelle/Récursion générale
Utilisation de Auto/EAuto (ajout de Hint dans la base)
Exemple
Développement sémantique
Formateurs
H. Herbelin
TP
exemple qui puisse amener à une approche reflexive

14h : Aspects avancés du langage de spécification

Objectifs de la séance
initier aux constructions evoluées du langage de spécification de Coq, comprendre comment ajouter des axiomes.
Durée
1h
Contenu
Arguments implicites, coercions, Record
constantes transparentes ou opaques.
Axiomes : Logique classique/ Extensionnalité/ Egalité
Formateur
H. Herbelin

15h00 : Définitions coinductives

Objectifs de la séance
Initiation à la représentation des objets infinis par des définitions co-inductives.
Durée
1h (cours-TD)
Contenu
Présentation des definitions co-inductives (type/ relation) sur des cas simples.
Formateur
C. Paulin

16h30 : Développer un exemple en sémantique

Objectifs de la séance
modéliser et prouver des propriétés d'un langage.
Durée
1h (TP)
Contenu
Formateurs
H. Herbelin & C. Paulin

3   Mercredi 27 février

Cette journée est l'occasion de présenter les outils évolués de Coq indispensables pour mener à bien des développements conséquents. Cette journée est accessible aux personnes ayant déjà une expérience de développement dans Coq ou bien ayant suivi la première journée de la formation.

9h30 : Adapter Coq à ses besoins

Objectifs de la séance
connaître les possibilités d'adaptation de Coq à un domaine particulier, Donner une idée du pouvoir d'automatisation de Coq

Durée
1h cours + 1h30 TD
Contenu
Introduire ses propres notations (Infix, grammaire)
Constructions de tactiques (Paramétrisation de Auto, AutoRewrite)
Construction de tactiques à toplevel (Tactic/Meta Definition)
Écriture de tactiques en ML (exemple d'une tactique utilisant une table)
Formateur
B. Barras
TP

14h : Coq outil de certification de programme

Objectifs de la séance
Donner un aperçu de la possibilité d'utiliser Coq pour certifier des programmes, application au développement de tactiques certifiées par des techniques de réflexion.
Durée
1h cours + 1h de TD
Contenu
Apercu des possibilités de Coq en matière de preuve de programmes
(Extraction/Refine/Correctness).
Le principe de la réflexion (Quote)
Formateur
J.-C. Filliâtre

16h30 : Développer une tactique certifiée

Objectifs de la séance
développer complètement une tactique de manière réflexive.
Durée
1h (TP)
Contenu
Formateurs
B. Barras & J.-C. Filliâtre
This document was translated from LATEX by HEVEA.