TypiCal

Intervenant : Alexandre Miquel (ENS Lyon)

Date et lieu : 16/04/2004, 10h, Salle de conférence du Lix

Résumé : Mon premier exposé sera consacré aux problèmes posés (en général) par l'extraction de programmes à partir de preuves formalisées en logique classique (i.e. avec tiers-exclu). Je commencerai par rappeler en quoi consiste l'extraction de programme dans le cadre de la logique constructive (i.e. sans tiers-exclu), les problèmes que cela pose et les différentes solutions proposées (typage vs. réalisabilité, extraction à la MinLog vs. extraction à la Coq...) Ensuite je m'intéresserai aux traductions négatives (qui servent à rétracter des théories classiques sur leur fragment constructif) et je montrerai comment ces traductions permettent de mettre en oeuvre (de manière effective) l'extraction de programmes à partir de preuves classiques de formules Pi_2. Enfin, je montrerai comment la théorie de la réalisabilité classique introduite par Krivine permet d'exprimer les mêmes programmes en style direct (i.e. sans CPS ni traduction négative) grâce à l'utilisation de continuations.