Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                        Amphi Turing du bâtiment 1

                             Lundi 2 mai, 10h30

                              ----------------
                              Alexandre Miquel
                              ----------------

                            Université Paris 7

    ===================================================================
    Une analyse calculatoire de la transformation de preuve par forcing
    ===================================================================

Le forcing est une technique inventée par Cohen pour démontrer la cohérence
et/ou l'indépendance de certains axiomes vis à vis de la théorie des
ensembles. Du point de vue de la théorie de la démonstration, le forcing
repose sur une traduction des formules et des preuves paramétrée par un
ensemble ordonné quelconque: l'ensemble des "conditions de forcing".
Récemment, Krivine a proposé une méthode permettant de combiner le forcing
avec la théorie de la réalisabilité classique, et a montré que la traduction
des preuves par forcing correspond (au niveau des termes de preuves à la
Curry) à une transformation de programme étonnamment compréhensible.

Suite aux travaux de Krivine, je montrerai comment reformuler le forcing en
arithmétique d'ordre supérieur, en me plaçant dans une extension adéquate du
système F-omega (classique) avec termes de preuves à la Curry. Je présenterai
la traduction des formules et la transformation de preuve-programme
sous-jacente. Enfin, j'analyserai le comportement calculatoire des programmes
traduits, et en déduirai une extension de la machine de Krivine avec
environnements explicites - la KFAM - conçue pour traiter directement les
preuves par forcing sans passer par la transformation de programme. Je
concluerai sur les liens que cette étude fait apparaître entre la méthode de
forcing et certains principes à la base des systèmes d'exploitation, ainsi que
sur les perspectives en logique.