Preuves assistées par ordinateur
Planning
TP:
mardi 16h30-18h30 (salle 548C), à partir du 26 janvier 2010
Cours:
mercredi 16h30-18h30 (salle 248E), à partir du 27 janvier 2010
Examen:
vendredi 21 mai 2010 15h30-18h30 (salle 470E)
Sujets de TD/TP
TD 1:
Premiers pas en Coq
(
correction
)
TD 2:
Déduction naturelle
TD 3:
Mathématiques élémentaires en Coq
(
correction
)
TD 4:
Preuves dans l'arithmétique de Peano
Principe du minimum
en Coq
TD 5:
Les entiers naturels en Coq
(
correction
)
TD 6:
Théories et modèles
TD 7:
Les listes en Coq
(
correction
)
TD 8:
Définitions inductives de prédicats
(
correction
)
TD 9:
Théorie des types simples et système T
TD 10:
Définitions inductives de prédicats et analyse par cas
(
correction
)
TD 11:
Équivalences de définitions arithmétiques
(
correction
)
Projet
Sujet du projet:
Théorème fondamental de l'arithmétique et théorème d'Euclide
.
Le projet est à faire
seul(e)
et comptera pour
la moitié
de la note finale (l'autre moitié étant l'examen écrit).
Le projet est à renvoyer
par mail
(merci de respecter l'adresse et le sujet) avant le samedi 1er mai 2010 à 18h30 (CEST).
Les soutenances auront lieu la semaine suivante.
Notes de cours (préparées par Alexandre Miquel)
Le
document principal
Le
système T
La
théorie des types simples de Church
Un
petit guide de survie
en Coq
Documents annexes
Un
tutorial
(en anglais) sur Coq
Le
manuel de référence de Coq
(en anglais)
Plus de détails à venir...
Dernière mise à jour: Tue Apr 6 15:29:37 CEST 2010.