To: seminaire@pauillac.inria.fr
From: Bruno.Barras@inria.fr
Subject: SEM - INRIA : LogiCal - 14/09/01 - Paris - FR

      Vous pouvez maintenant vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html


                             S E M I N A I R E
                                         . ___ 
                           /   _   _      /   _   /
                          /   / \ / \  / /   __| /
                         |___ |_/ |_/ / |__ |_/ |_
       ___      .                  /    
      /    ___   __  /_  _   /   _/        /| /|  _   __ __ _       _ 
     /    /   / /_  /   __| /             / |/ | / \ /_ /  / \ | / __|
    |___ /   / __/ |_  |_/ |_            /     | |_/__/ |_ |_/ |/ |_/
                                                
                          I N R I A - Rocquencourt
                       Salle de conference du Bat 11

                        Vendredi 14 septembre, 10h30

                             ------------------
                             Jean-Marc Andreoli
                             ------------------

                        Xerox Research Centre Europe

        ============================================================
        Vers un paradigme de programmation fondé sur la construction
                       de preuves en Logique Linéaire
        ============================================================


    Prolog fut un  des premiers paradigmes de programmation  fondés sur la
    recherche  de preuve.   Il eut  un  certain succès  dans des  domaines
    d'application particuliers,  par exemple en  Intelligence Artificielle
    ou en Linguistique Computationnelle.  Pour dépasser les limites de ces
    cadres, de nombreuses extensions ont été proposées, avec plus ou moins
    de succès.  Certaines propositions,  notamment autour du traitement de
    la  négation, étaient  conçues de  manière trop  ad-hoc  pour résoudre
    certains problèmes  spécifiques. D'autres approches,  en revanche, ont
    une  portée beaucoup  plus large:  initiées avec  Lambda-Prolog, elles
    ré-interprètent le paradigme en terme  du calcul des séquents (au lieu
    de  la traditionnelle  Résolution),  et  s'ouvrent par  là  même à  de
    nouveaux systèmes, au  delà de la Logique Classique,  comme la Logique
    Intuitionniste, Linéaire, et, plus récemment Non-Commutative. Dans une
    première partie de l'exposé, je  passerai en revue quelques uns de ces
    systèmes,  qui, malgrè  leurs fondements  théoriques  solides, restent
    d'usage limité (voire confidentiel)  dans la pratique. Une des raisons
    de  cet  insuccès (relatif)  est  l'absence  de domaine  d'application
    privilégié et de différentiel clair vis-à-vis de langages généralistes
    qui reposent sur  une sémantique sans doute moins  claire mais restent
    beaucoup plus  performants. Dans une  deuxième partie de  l'exposé, je
    présenterai un domaine d'application dans lequel, dans mon expérience,
    le  paradigme de  recherche  de preuve,  plus  précisément en  Logique
    Linéaire, prend  tout son intérêt  et permet d'apporter  des solutions
    originales au delà de  la reformulation élégante de mécanismes connus.
    Il  s'agit  de la  conception  de  plateformes  pour le  développement
    d'applications réparties (systèmes  dit "middleware"). Je montrerai en
    particulier  comment la  notion  centrale de  ressource,  issue de  la
    Logique Linéaire, permet modéliser  et mettre en oeuvre des mécanismes
    récurrents  dans  de  nombreuses  applications  réparties  (mécanismes
    appelés "services  infrastructurels" dans  la terminologie de  l'OMG -
    Object Management Group). Cette approche a été exploitée en profondeur
    dans le projet  CLF au XRCE. Enfin, je  présenterai également quelques
    perspectives de ce travail, notament  dans la direction des réseaux de
    preuves.

    A propos du présentateur: http://www.xrce.xerox.com/~andreoli