Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Formation à l'assistant de preuve COQProgramme provisoire
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)
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.