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
2006 - 2007
Fondements des systemes de preuves
Alexandre Miquel
,
Gilles Dowek
Théorie des types (polycopié)
System F (lecture notes)
Normalisation of second order arithmetic (lecture notes)
Travaux Pratiques en Coq
Alexandre Miquel
Petit guide de survie en Coq
TP 1
TP 1 - corrigé
TP 2
TP 2 - corrigé
TP 3
TP 3 - corrigé
TP 4
TP 4 - corrigé
TP 5
TP 5 - corrigé
TP 6
TP 7
TP 8
Assistants de preuves
Christine Paulin-Mohring
,
Jean-Christophe Filliâtre
,
Bruno Barras
,
Hugo Herbelin
,
Benjamin Werner
,
Claude Marché
Polycopié du cours
Preuve de programmes fonctionnels
Jean-Christophe Filliâtre
Transparents Cours 1
Transparents Cours 2
Transparents Cours 3
Transparents Cours 4
Transparents Cours 5
Projet
Jean-Christophe Filliâtre
,
Hugo Herbelin
Projet : sujet (implémenter un type checker pour mini-Coq)
Projet : fichiers tests
Projet : parseur fourni (Ocaml)