Différences

Ci-dessous, les différences entre deux révisions de la page.

--- formations:masters:ue:m1:pao8 [2023/05/22 15:29] – supprimée - modification externe (Date inconnue) 127.0.0.1
+++ formations:masters:ue:m1:pao8 [2025/01/29 10:46] (Version actuelle) – ↷ Liens modifiés en raison d'un déplacement. admin
@@ Ligne 1: / Ligne 1: @@
+~~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

Outils pour utilisateurs

Outils du site

Différences

Outils de la page