Enseignant : Christine Paulin-Mohring
Documents référencés
Pour voir les documents d’une ressource écrits par d’autres enseignants, cliquez sur son titre, ou bien sur son icône ou .
Thème : Logique & Preuve –
Cursus : MPRI - M2 Bruno Barras , Christine Paulin-Mohring - 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)
Bruno Barras , Christine Paulin-Mohring