| Résume | La logique de la programmation s'est développée depuis la mise en évidence des liens étroits qu'entretiennent théorie de la démonstration et théorie de la programmation. La correspondance, dite de Curry-Howard, entre
1) formules logiques et types de données
2) preuves et programmes
3) élimination des coupures (ou normalisation de preuve) et exécution d'un programme
a stimulé une intense activité visant à comprendre le contenu logique des structures de programmation et le contenu calculatoire des formes du raisonnement ou des axiomes logico-mathématiques et a renouvelé les perspectives sur la programmation comme sur la théorie de la démonstration.
Dans cet exposé, on s'intéressera à diverses formes de raisonnements par induction, de la récurrence usuelle à la descente infinie, et aux systèmes de preuves qui les formalisent. Je considérerai notamment des logiques à points fixes (dérivées du mu-calcul, qui permettent d'exprimer aussi bien des enoncés inductifs que coinductifs), dans lesquelles j'étudierai des systèmes de preuves non bien-fondés où les dérivations sont des arbres potentiellement infinis (éventuellement réguliers). Je présenterai les principaux résultats de la théorie de la démonstration infinitaire (en particulier l'élimination des coupures), ses relations avec les preuves finitaires ainsi que des perspectives d'application à la programmation. |
