Accueil
Connexion
DENIF –
Documents d’Enseignement Numériques en Informatique Fondamentale
Thèmes
Cursus
Enseignants
Assistants de preuves et leur théorie
Thème :
Logique & Preuve
–
Cursus :
MPRI - M2
2007 - 2008
Cours
Christine Paulin-Mohring
,
Bruno Barras
Polycopié (PS)
Polycopié (PDF avec feuilles dans le bon sens)
Cours 1 : Calcul des Constructions au Calcul des Constructions Inductives
Cours 2 : Les spécificités du Calcul des Constructions Inductives
Cours 3 : Programmation fonctionnelle 1
Cours 4 : Programmation fonctionnelle 2
Cours 5 : Types dépendants, extraction
Cours 6 : Programmation impérative
Cours 7 : Panorama et architecture des assistants de preuve
Cours 8 : Modèles de réalisabilité et modèles booléens
TDs
TD 1
TD 1 - corrigé
TD 1 - Coq
TD 2
TD 2 - corrigé
TD 2 - Coq
TD 3
TD 3 - Coq
TD 4
TD 4 - Template
TD 5
TD 5 - Exemple du cours
TD 6
TD 8
TD 8 - Corrigé
Examens
2007-2008
2006-2007
2005-2006
2004-2005
2003-2004
2002-2003
2001-2002
Projets des années passées
Preuves automatiques en Arithmétique
Mini-Coq
Tactique réflexive de dérivation formelle
Arithmétique de Peano en Coq
Fonctions récursives et machines de Minski
Réalisabilité
Constructions par point fixe