Cours Preuves assistées par ordinateur (hiver 2024)

Horaires

12 semaines à partir du 26 janvier 2024 (à partir du 26 janvier aussi pour les TD / TP).

• Cours : vendredi 10h45-12h45, salle 2001 (Hugo Herbelin)
• TP/TD : vendredi 16h15-18h15, salle 1003 (Thierry Martinez)

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

Projet

Le projet sera donné ultérieurement.

Examens

• examen 2021 avec sa correction et le code Coq correspondant

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

• examen 2023 avec sa correction