Preuves assistés par ordinateur

es assistants à la preuve sont des logiciels permettant de définir des objets mathématiques (tels que les entiers, les groupes, les anneaux) ou informatiques (tels que les entiers machine, l'addition, les graphes, les arbres, les programmes), ainsi que des propriétés de ces objets (tel que être premier, être commutatif, être fini, être égal, être terminant), et de prouver des théorèmes sur ces propriétés.

Le cours et les TDs de ce module alterneront théorie et pratique avec pour double objectif d'introduire à l'utilisation des assistants à la preuve, et d'en décrire les fondations logiques, à commencer par la correspondance entre preuves et programmes qui dit notamment qu'une preuve que A implique B en logique, c'est la même chose qu'un programme qui prend un argument de type A et renvoie un argument de type B.

1. Formalisme logique de la déduction naturelle intuitionniste
2. Procédure de normalisation, coupures commutatives, dualité introduction-élimination, dualité positif-négatif
3. Lambda-calcul simplement typé, formes normales, β-réduction, règles η, contextes d'évaluation
4. Correspondance entre preuves et programmes et entre propositions et types
5. Théorèmes principaux : confluence, normalisation, préservation du typage, propriété de la sous-formule, inversibilité de l'introduction des connecteurs négatifs et de l'élimination des connecteurs positifs, admissibilité de la contraction, de l'affaiblissement, de l'échange
6. Logique classique et opérateurs de contrôle
7. Entiers et autres types inductifs, itérateur, récurseur, analyse de cas, récursion bien fondée, récursion gardée et non gardée, coinduction
8. Système T, Système F, Système Fω, systèmes de types purs
9. Une hiérarchie de force logique et d'expressivité calculatoire (PRA, PA, PA₂,ZF)

Cours Programmation Fonctionnelle du L3 :

• Programmation fonctionnelle en OCaml
• Programmer avec des structures de données algébriques (arbres) en OCaml

Autres modules utiles :

1. Cours Compilation du M1 :
   • Systèmes de typage
2. Cours Logique du L3 :
   • Connecteurs de la logique propositionnelle
   • Calcul des séquents
3. Cours Machines virtuelles du L3 :
   • Machines à pile
   • Données structurées
   • Fonctions et notion de clôture