BAR-RÉCURSION, ANALYSE ET RÉALISABILITÉ CLASSIQUE Hadrien Batmalle, IRIF Salle B107, bâtiment B, Université de Villetaneuse 16/06/2017 11:00 - 12:30 Résumé : La réalisabilité classique est une théorie née des travaux de Jean-Louis Krivine dans les années 1990, à la frontière entre la logique et l'informatique théorique. Côté informatique, elle offre un cadre adapté à l'interprétation calculatoire de preuves classiques. Côté logique, elle apparaît comme une généralisation prometteuse du forcing de Cohen. À un modèle du lambda-calcul, on peut ainsi associer un modèle de la théorie des ensembles ZF. On s'intéresse ici à des modèles de programmation vérifiant une propriété de continuité: il peut s'agir de modèles basés sur les domaines de la sémantique dénotationnelle, ou bien de modèles de termes d'une version infinitaire du lambda-calcul. Dans ces modèles, l'instruction 'quote' (qu'on utilise usuellement en réalisabilité classique pour interpréter l'axiome du choix dépendant) n'est pas disponible. On utilise donc la technique de la bar-récursion pour interpréter l'axiome du choix dépendant. Or (en considérant la réalisabilité classique comme une généralisation du forcing), il apparaît que la bar-récursion est de plus l'analogue de la condition de chaîne descendante dans les algèbres de forcing (qui correspond à une propriété de préservation des réels). On obtient alors que toute formule de l'analyse vraie dans le modèle ambiant est réalisée dans ces nouveaux modèles, ce qui nous amène à la question suivante: quel est le comportement des programmes réalisant des formules de l'analyse?