Cours Preuves assistées par ordinateur (hiver 2023)

Horaires

12 semaines à partir du 18 janvier 2023 (à partir du 20 janvier pour les TD / TP).

• Cours : mercredi 10h45-12h45, salle Condorcet 86A (Hugo Herbelin)
• TP/TD : vendredi 11h-13h, salle 2001 (Théo Zimmermann)

Objectifs du cours

Dans une société toujours plus dépendante du bon fonctionnement des programmes informatiques, le cours combinera une introduction aux principes de base de la preuve des programmes (la logique) et une introduction à l'utilisation du logiciel Coq pour la preuve de correction effective des programmes.

Notes de cours

• Introduction à la logique du 1er ordre (notes d'Alexandre Miquel pour la version initialle du cours en 2008)
• Notes de cours sur la correspondance preuve-programme, notamment en logique classique (en anglais)
• Un petit guide de survie pour Coq

Plan prospectif

• Cours 1 : Contexte historique, règles d'inférence de la déduction naturelle (section 2.1 du poly PP)
• Cours 2 : Règles d'inférence de la déduction naturelle (suite), lambda-calcul simplement typé, β-réduction, correspondance preuves-programmes (section 3.1 du poly PP), quantificateurs
• Cours 3 : Lambda-calcul simplement typé, correspondance preuves-programmes, élimination des coupures, propriété de la sous-formule (Théorème 5 du poly PP), formes normales, normalisation
• Cours 4 : Règles η, inversibilité de l'introduction des connecteurs négatifs et de l'élimination des connecteurs positifs, admissibilité de la contractione et de l'affaiblissement
• Cours 5 : Coupures commutatives, logique classique et opérateurs de contrôle, contextes d'évaluation
• Cours 6 et 7 et 8 : Types inductifs, itérateur / récurseur / analyse de cas / point fixe / récurrence / analyse de cas dépendante
• Cours 9 : Coq's match/fix, récursion gardée, système F, codage de Church
• Cours 10 : Une hiérarchie de force logique et d'expressivité calculatoire (PRA, PA, PA₂, ZF)
• Cours 11 : coinduction
• Cours 12 : Familles inductives
• Cours 12 : Synthèse

Séances TP / TD

• Séance 1 (20 janvier) : TD 1 (correction)
• Séance 2 (27 janvier) : Suite du TD 1
• Séance 3 (3 février) : TP 1
• Séance 4 (10 février) : Suite du TD 1
• Séance 5 (17 février) : TP 2
• Séance 6 (24 février) : TD 2
• Séance 7 (10 mars) : TP 3
• Séance 8 (17 mars) : TP 4
• Séance 9 (24 mars) : TP 5
• Séance 10 (31 mars) : TP 6
• Séance 11 (7 avril) : Suite du TD 2
• Séance 12 (14 avril) : TP 7

Projet

Cf. projet/README.md

Examens

• examen 2021 avec sa correction et le code Coq correspondant

• examen 2022 avec sa correction partielle et le code Coq correspondant