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

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 L^AT_EX by H^EV^EA.