~~NOTOC~~

====== Preuves assistés par ordinateur ======


===== Description =====

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.


===== Syllabus =====
==== Sujets centraux ====

  - Formalisme logique de la déduction naturelle intuitionniste
  - Procédure de normalisation, coupures commutatives, dualité introduction-élimination, dualité positif-négatif
  - Lambda-calcul simplement typé, formes normales, β-réduction, règles η, contextes d'évaluation
  - Correspondance entre preuves et programmes et entre propositions et types
  - 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
  - Logique classique et opérateurs de contrôle
  - 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
  - Système T, Système F, Système Fω, systèmes de types purs
  - Une hiérarchie de force logique et d'expressivité calculatoire (PRA, PA, PA₂,ZF)


===== Pré-requis =====

Cours [[..:..:..:licence:2024-2025:ue:l3:pf5|Programmation Fonctionnelle]] du L3 :
  * Programmation fonctionnelle en OCaml
  * Programmer avec des structures de données algébriques (arbres) en OCaml

Autres modules utiles :

  - Cours [[com7|Compilation]] du M1 :
    * Systèmes de typage
  - Cours [[..:..:..:licence:2024-2025:ue:l3:lo5|Logique]] du L3 :
    * Connecteurs de la logique propositionnelle
    * Calcul des séquents
  - Cours [[..:..:..:licence:2024-2025:ue:l3:mv6|Machines virtuelles]] du L3 :
    * Machines à pile
    * Données structurées
    * Fonctions et notion de clôture