SÉMINAIRE 2007-08

Responsable : Virgile MOGBIL (téléphone : 01 49 40 36 84).
Horaire : le lundi à 15h30.
Lieu : Laboratoire d'informatique de Paris-Nord (comment y venir).
Salle B311 (Institut Galilée, 3e étage du batiment B).
Archives: séminaire 2001-02, 2002-03, 2003-04, 2004-05, 2005-06, 2006-07.

Lundi 9 juin 2008, salle B311 à 15h30 : Paulin Jacobé de Naurois (LIPN),
Titre : Correctness of Multiplicative Additive Proof Structures is NL-Complete.
Résumé : We revisit the correctness criterion for the multiplicative additive fragment of linear logic. We prove that deciding the correctness of corresponding proof structures is NL-complete (Joint work with V. Mogbil).

Lundi 2 juin 2008 (scéance double), salle B311
- à 15h30 : Kais Klai (LIPN), titre : MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs.
- à 16h30 : Laure Petrucci (LIPN), titre : Modular Construction of the Symbolic Observation Graph.
Résumé de Kais Klai : Model checking is a powerful and widespread technique for the verification of finite distributed systems. However, the main hindrance for wider application of this technique is the well-known state explosion problem. During the last two decades, numerous techniques have been proposed to cope with the state explosion problem in order to get a manageable state space. Among them, on-the-fly model-checking allows for generating only the "interesting" part of the model while symbolic model-checking aims at checking the property on a compact representation of the system by using Binary Decision Diagram (BDD) techniques. In this work, we propose a technique which combines these two approaches to check LTL\X state-based properties over finite systems. During the model checking process, only an abstraction of the state space of the system, namely the symbolic observation graph, is (possibly partially) explored. The building of such an abstraction is guided by the property to be checked and is equivalent to the original state space graph of the system w.r.t. LTL\X logic (i.e. the abstraction satisfies a given formula f iff the system satisfies f). Our technique was implemented for systems modeled by Petri nets and compared to an explicit model-checker as well as to a symbolic one (NuSMV) and the obtained results are very competitive.
Résumé de Laure Petrucci : Model checking for Linear Time Logic (LTL) is usually based on converting the (negation of a) property into a Büchi automaton, composing the automaton and the model, and finally checking for emptiness of the language of the composed system. The last step is the crucial stage of the verification process because of the state explosion problem. In this work, we present a solution which builds, in a modular way, an observation graph represented in a non-symbolic manner but where the nodes are essentially symbolic sets of states and the edges either labeled by events occurring in the formula or by synchronization actions between the system components. Due to the small number of events to be observed in a typical formula, this graph has a very moderate size and thus the time complexity for verification is negligible w.r.t. the time to build the observation graph. Experimental results show that our method outperforms both a non-modular generation of the symbolic graph and existing non-symbolic approaches (modular or not).

Lundi 14 avril 2008, salle B311 à 15h30 : Sylvain Lippi (I3S, Université de Nice).
Titre : L'interaction dure.
Résumé : Les systèmes durs, une sous-classe des réseaux d'interaction, se présentent sous la forme de systèmes de re-étiquetage de graphes fortement confluents. Nous présentons quelques traductions dans des sous-classes des systèmes durs et en déduisons quelques idées simples sur l'universalité. En particulier, nous donnons une traduction dans un système universel à 7 règles.

Lundi 7 avril 2008, salle B311 à 15h30 séminaire d'une heure : Faouzi Boufares (LIPN), Sana Hamdoun (LIPN) et Mohamed Badri (CRIP5 - LIPN - Université Paris 5).
Titre : Construction et maintenance d'entrepôts de données.
Résumé : Les données nécessaires à des fins décisionnels sont de plus en plus complexes. Elles ont des formats hétérogènes et proviennent de sources distribuées. Elles peuvent être classées en trois catégories : les données structurées, les données semi-structurées et les données non-structurées. Dans cet exposé, nous présentons le processus d'intégration de données dans le but de construire un entrepôt dont les sources sont totalement hétérogènes. Nous proposons un cadre formel qui se base sur la définition d'un environnement d'intégration. Nous présentons également notre processus de maintenance d'entrepôt de données qui assure à la fois la mise à jour du contenu de l'entrepôt et l'actualisation des agrégats (indicateurs décisionnels) calculés sur les données de l'entrepôt.

Mardi 11 mars 2008, Amphitéatre Euler, Institut Galilée, à 14h00 : soutenance d'habilitation à diriger les recherches de Patrick Baillot (LIPN).
Titre : Logique Linéaire, Types et Complexité Implicite.
Résumé

6 et 7 mars 2008, Amphitéatre Euler, Institut Galilée, Villetaneuse : réunion des groupes de travail nationaux GEOCAL (Géométrie du calcul) et LAC (Logique, Algèbre et Calcul), dans le cadre du GDR-IM (Informatique Mathématique), 50 participants.

11, 12 et 13 Février 2008, Amphitéatre Copernic, Institut Galilée, Villetaneuse : workshop on Implicit Computational Complexity, dans le cadre du projet ANR NO-CoST (LIPN/PPS), 40 participants dont 20 étrangers de 10 pays.

Lundi 4 Février 2008 (scéance double), salle B311
- à 14h30 : Antonino Salibra (Università Ca'Foscari di Venezia), titre : From Universal Algebra and Topology to Lambda Calculus and Back.
- à 15h30 : Alexandre Miquel (PPS - Université Paris 7), titre : Extraction de programmes classique dans le Calcul des Constructions.
Résumé d'Antonino Salibra : In this seminar we show how algebra and topology can be fruitfully applied to the operational semantics and to the model theory of the untyped lambda calculus. We explain the structure of the lattice of lambda theories (i.e., equational extensions of lambda calculus) and analyze one of the long-standing open problem of lambda calculus, regarding the existence of a topological model of the beta-eta lambda theory, where all Scott-continuous functions are representable.
Résumé d'Alexandre Miquel : Dans cet exposé, je me propose de montrer que les techniques de réalisabilité classique introduites par Jean-Louis Krivine sont compatibles avec le Calcul des Constructions avec univers (CCw), et qu'elles permettent d'envisager un mécanisme d'extraction de programme à partir de preuves classiques (avec proof-irrelevance et axiome du choix) formalisées en Coq (dans la sorte Prop).
Pour cela, je commencerai par rappeler ce qu'est la réalisabilité classique au sens de Krivine (langage et modèles). Ensuite je montrerai comment étendre le modèle de réalisabilité de Krivine (initialement défini pour l'arithmétique du second ordre) à CCw, en utilisant une structure de Pi-set réminiscente des structures de omega-set (Hyland, Longo, Moggi), de D-set (Streicher) et de lambda-set (Altenkirch). Enfin, je présenterai un certain nombre de pistes pour étendre ce schéma d'extraction aux types inductifs (notamment les entiers) en utilisant des structures de données efficaces dans le langage cible (entiers binaires).

Lundi 7 Janvier 2008, salle B107 à 15h30 : Benoît Valiron (University of Ottawa).
Titre : Semantics for higher-order quantum computation.
Résumé : We give a categorical semantics for a call-by-value linear, computational lambda calculus and discuss some steps towards a concrete model. Such a lambda calculus was used by Selinger and Valiron as the backbone of a functional programming language for quantum computation. One feature of this lambda calculus is its linear type system, which includes a duplicability operator "!" as in linear logic. Another main feature is its call-by-value reduction strategy, together with a side-effect to model probabilistic measurements.

Lundi 17 Décembre 2007, salle B107 à 15h30 : Yves lafont (IML - Université de la Méditerranée). Notez la salle inhabituelle.
Titre: Réécriture de la géométrie (en collaboration avec Pierre Rannou)
Résumé : Ce travail, vaguement inspiré par la recherche sur le calcul quantique, s'inscrit dans un programme de recherche plus vaste intitulé "Géométrie de la réécriture".
On représente les matrices orthogonales réelles (ou les isométries de R^n) par des "circuits orthogonaux" construits avec deux types de portes : la symétrie (porte unaire) et les rotations (portes binaires). On obtient ainsi un système de réécriture de diagrammes qui est à la fois noetherien et confluent. La forme normale généralise la "décomposition d'Euler". La confluence est évidente, mais l'étude des paires critiques conduit à une description axiomatique de la fonction permettant de passer d'une décomposition d'Euler à l'autre en dimension 3. En particulier, on retrouve l'"équation du tétraèdre", aussi appelée équation de Zamolodchikov, bien connue des physiciens théoriciens.
Référence : Y. Lafont, Towards an Algebraic Theory of Boolean Circuits, Journal of Pure and Applied Algebra 184 (2-3), p. 257-310, Elsevier (2003)

Lundi 26 Novembre 2007, salle B311 à 15h30 : Laurent Poinsot (LIPN).
Titre: Fonctions parfaitement non linéaires et actions de groupe.
Résumé : Les boîtes-S des procédés de chiffrement (à clef secrète) par blocs itéré sont notamment conçues pour résister aux attaques différentielle et linéaire. Ces cryptanalyses reposent sur la manière de combiner le texte clair et la clef. L'opération de combinaison traditionnellement employée est l'addition bit-à-bit de vecteurs binaires. Il existe d'autres façons de mélanger le clair et la clef, aussi dans cet exposé on se propose de remplacer l'addition par une action de groupe plus générale. On étudie alors l'attaque différentielle adaptée à cette nouvelle opération de combinaison ainsi que les boîtes-S qui lui opposent la meilleure résistance possible. On montre en particulier que l'on peut construire des fonctions robustes dans des cas où leurs homologues classiques (i.e. lorsque l'opération de combinaison est une addition binaire) n'existent pas.
Slides : download.

Lundi 12 Novembre 2007, salle B311 à 15h30 : Céline Rouveirol (LIPN).
Titre: Petit Voyage au pays de la Programmation Logique Inductive
Résumé : Je présenterai une brève introduction à la Programmation Logique Inductive, qui s'intéresse aux modèles logique de l'apprentissage supervisé et plus largement à l'apprentissage supervisé dans les langages de concepts restrictions de la logique d'ordre un. Je motiverai ce type d'apprentissage, je détaillerai les modèles logiques les plus utilisés en Programmation Logique Inductive et quelques travaux fondateurs, pour enfin pointer vers quelques problématiques prometteuses.

Lundi 5 Novembre 2007, salle B311 à 15h30 : Michele Basaldella (Università di Siena).
Titre: Exponentials in Ludics: How and at what price.
Résumé : Ludics is a research project introduced by J-Y Girard in 2001 whose aim is to overcome the distinction Syntax/Semantics (of proofs) and it consists of a theory in which both sides deal with objects of the same nature, Design, which are basic artifacts of Ludics. They are manipulated by means of cut-elimination, conceived as the unique tool for testing properties inside the theory itself. Ludics also provides a (fully complete) Game Semantics for Multiplicative Additive Focalized Linear Logic. In this talk, we will show how to extend Ludics framework by adding exponential constructions in such a way to preserve the Ludics Theorems (in particular Separation Theorem). As we will see, our approach is closely related to AJM Game Semantics in the treatment of exponentials. We will also discuss the limits of our framework as well as its strength, namely the preservation of all isomorphisms involving exponentials, and the arising of a notion of non uniform exponential, both appearing in a rather natural way.

Lundi 8 Octobre 2007, salle B311 à 15h30 : Christophe Fouqueré (LIPN).
Titre: Calcul Logique pour Multiséquents
Résumé : Un Calcul logique gérant des multiséquents est présenté. Ce calcul est motivé par une réflexion sur l'évaluation paresseuse en programmation logique, ou encore la concurrence stricte et l'interférence. Le calcul introduit deux nouveaux connecteurs gérant la structure de multiséquents. C'est une extension conservative de la Logique Linéaire, permettant l'élimination des coupures. On proposera une sémantique des phases. Si le temps le permet, on évoquera des extensions du calcul.

10, 11 et 12 septembre 2007, Institut Henri Poincaré, Paris : Journées Jean-Yves Girard, conférence en l’honneur de son 60e anniversaire