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.