Thème : Logique & Preuve –
Cursus : MPRI - M2 Christine Paulin-Mohring , Bruno Barras - 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)