README.md

Cours Preuves assistées par ordinateur (hiver 2025)

Horaires

12 semaines à partir du 24 janvier 2025 (à partir du 24 janvier aussi pour les TD / TP).

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

Attention: Inversion des créneaux cours/TDs à partir du 7 février.

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, correspondance preuve-programme pour la déduction naturelle propositionnelle
• 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