herbelin/cours-preuves-ordinateur
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
Page du cours preuves assistées par ordinateur 2021
118 commits 1 branch 0 tags 5.1 MiB
  • TeX 80.5%
  • Rocq Prover 19.5%
Find a file
Exact
Thierry Martinez d36cd40ade
 Correction exists
2025-05-16 11:22:37 +02:00
an_introduction_to_coq Sujet TP no 1 + intro à coq 2025-01-31 14:57:36 +01:00
examens Ajout examen 2024 2025-05-15 12:13:06 +02:00
projet Place libre pour nouveau projet 2024-01-16 15:01:36 +01:00
projets Correction exists 2025-05-16 11:22:37 +02:00
td Correction date 2025-03-14 10:44:13 +01:00
tp Ajout TP 3 2025-03-21 09:57:15 +01:00
.gitignore Sujets des TP. 2021-01-17 21:37:12 +01:00
contexte-historique.pdf MAJ 2025-01-25 21:17:45 +01:00
LICENSE Initial commit 2021-01-15 15:41:57 +01:00
logique-premier-ordre.pdf Notes 2021-01-15 17:17:39 +01:00
proofs-and-programs.pdf MAJ poly preuves/programmes 2021-02-07 21:55:25 +01:00
README.md Ajout examen 2024 2025-05-15 12:13:06 +02:00

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

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 est décrit ici

Examens antérieurs