Séminaires : Séminaire Général de Logique

Equipe(s) : lm,
Responsables :O. Finkel, T. Ibarlucía, A. Khélif, S. Rideau, C. Sureson
Email des responsables :
Salle : salle 2015
Adresse :Sophie Germain
Description

ArchivesRetour ligne automatique
Abonnement à la liste de diffusion


Orateur(s) Alexis Saurin - Institut de Recherche en Informatique Fondamentale (IRIF) - Université Paris 7,
Titre Logiques à points fixes et théorie de la preuve (in)finitaire
Date30/05/2016
Horaire15:10 à 16:10
RésumeDans 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.
Sallesalle 2015
AdresseSophie Germain
© IMJ-PRG