Calcul des Constructions Inductives
DEA Sémantique, Preuves et Langages 2003-2004
Lundi 11h-13h Chevaleret salle 0D1
Enseignants
Plan
-
Semaine 1 : 5 janvier-HH
- Introduction, Définitions Inductives
- Semaine 2 : 12 janvier-HH
- Exemple de mise en oeuvre de
définitions inductives
- Semaine 3 : 19 janvier
- 10h-13h Travaux Pratiques Coq salle 1C22
Sujet.
- Semaine 4 : 26 janvier-CP
- Théorie des définitions
(co)inductives (1)
- Semaine 5 : 2 février-CP
- Théorie des définitions
(co)inductives (2)
- Semaine 6 : 9 février-JCF
- Preuve Programmes fonctionnels, Extraction
- Semaine 7 : 23 février-CM
- Preuve Programmes imperatifs, outils
- Semaine 8 : 1 mars-CP
-
Automatisation-Architecture d'un système de preuve, Preuve par réflexion
- Semaine 9 : 8 mars-HH
- Sémantique, Paradoxes
- Semaine 10
- Soutenances de projet/Examen
Notes de cours
Postscript-double page
Le cours complet
Par chapitre :
Projet
L'évaluation de cet enseignement est faite sur un examen ou
(non-exclusif) un projet, la note maximale étant retenue. Le projet
est a réaliser individuellement avec le système Coq, il consiste à
modéliser un compilateur des fonctions récursives vers des machines de
Minsky. Le projet est à rendre la semaine du 22 mars et les
soutenances auront lieu le lundi 29 mars.
Projet 2004 (ps) Projet 2004 (pdf)
Quelques sujets d'examen, projets
-
2002/2003
- Examen/Projet
- 2001/2002
- Examen/Projet
This document was translated from LATEX by
HEVEA.