DENIF – Documents d’Enseignement Numériques en Informatique Fondamentale

     Fondements des systèmes de preuves : TPs  

•   TP1
•   TP2
•   TP3
•   TP4
•   TP5
•   TP6
•   TP7
•   TP8

     Assistants de preuve : cours  

•   Notes de cours
•   Cours 1 (du Calcul des Constructions au Calcul des Constructions Inductives)
•   Cours 2 (les spécificités du Calcul des Constructions Inductives)
•   Cours 3 (programmation fonctionnelle 1, récursion structurelle versus accessibilité, fonctions partielles, définitions co-inductives)
•   Cours 4 (programmation fonctionnelle 2, constructions monadiques, modules, preuves automatiques versus preuves interactives, applications: preuve par réflexion)
•   Cours 5 (architecture d'un système de preuve, langages de tactiques)
•   Cours 6 (modèles de réalisabilité et modèles booléens)
•   Cours 7 (types dépendants, extraction)
•   Cours 8 (programmation impérative, Why, preuve de programmes C ou Java)

     Assistants de preuves : TDs  

•   TD 1
•   TD 1 : corrigé
•   TD 1 : code Coq
•   TD 2
•   TD 3
•   TD 3 : code Coq
•   TD 4
•   TD 4 : code Coq
•   TD 7
•   TD 8

     Cours

•   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

     Fondements des systemes de preuves  

•   Théorie des types (polycopié)
•   System F (lecture notes)
•   Normalisation of second order arithmetic (lecture notes)

     Travaux Pratiques en Coq  

•   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  

•   Polycopié du cours

     Preuve de programmes fonctionnels  

•   Transparents Cours 1
•   Transparents Cours 2
•   Transparents Cours 3
•   Transparents Cours 4
•   Transparents Cours 5

     Projet  

•   Projet : sujet (implémenter un type checker pour mini-Coq)
•   Projet : fichiers tests
•   Projet : parseur fourni (Ocaml)