| Résume | Dans cet exposé, on étudiera la théorie de la démonstration de logiques à points fixes, en se plaçant dans le cadre de la correspondance de Curry-Howard qui met en relation 1) formules logiques et types de données 2) preuves et programmes 3) procédure d'élimination des coupures et exécution d'un programme.
L'exposé conduira à discuter du contenu calculatoire des logiques à points fixes et permettra de présenter des systèmes de preuves finitaires et infinitaires pour ces logiques. En se concentrant sur le cadre infinitaire, on présentera les théorèmes de focalisation et d'élimination des coupures, résultats centraux en théorie de la démonstration, notamment pour la logique linéaire, que l'on introduira, resituera et dont on discutera les conséquences. |
