SÉMINAIRE 2006-07

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

Semaine du 25 Juin : RDP 2007

Lundi 25 Juin 2007, à 11h00 : Max Kanovich (Queen Mary, Univ. of London),

Title: Missing Opportunity: Light Linear Logic with Controlled Weakening
Abstract: Starting from Girard's seminal paper on light linear logic (LLL), a number of works investigated on systems derived from linear logic and corresponding to computational complexity classes. The intuitionistic fragments of a number of systems are shown to capture polynomial time computation within the computation-as-cut-elimination paradigm. However, the underlying light logics do not behave well with respect to any choice of cut reduction strategies. Thus the original LLL has been proved to be only weakly polytime sound, where, in particular, only a {\em lazy} cut-elimination over the so-called additive connectives is allowed. Asperti's Intuitionistic Light Affine Logic works well as a calculus of intuitionistic proof-nets or as Terui's term calculus (the latter enjoys polytime strong normalization), but a {\em lazy} cut-reduction is needed in the classical version of Light Affine Logic due to unrestricted weakening. The original syntax of LLL is too complicated, mainly because one has to deal with sequents which not just consist of formulas but also of `blocks' of formulas. We circumvent the complications of `blocks' by introducing a new modality $\nabla$ which is exclusively in charge of `additive blocks'. The most interesting feature of this purely multiplicative $\nabla$ is the possibility of the second-order encodings of additive connectives. The resulting system (with the traditional syntax), called Easy-LLL, is still powerful to represent any deterministic polynomial time computations in purely logical terms. Unlike the original LLL and the classical version of light affine logic, Easy-LLL admits polynomial time strong normalization, namely, cut elimination terminates in a unique way in polytime by any choice of cut reduction strategies. The elementary version of the logic has the corresponding elementary time properties.

Lundi 18 Juin 2007, salle B311 à 16h00 : Kais Klai (LIPN).

Title: An Incremental Modular Technique for Checking LTL-X Properties on Petri nets
Abstract: Model-checking is a powerful and widespread technique for the verification of finite state concurrent systems. However, the main hindrance for wider application of this technique is the well-known state explosion problem. Modular verification is a promising natural approach to tackle this problem. It is based on the "divide and conquer" principle and aims at deducing the properties of the system from those of its components analysed in isolation. Unfortunately, several issues make the use of modular verification techniques difficult in practice. First, deciding how to partition the system into components is not trivial and can have a significant impact on the resources needed for verification. Second, when model-checking a component in isolation, how should the environment of this component be described? In this work, we address these problems in the framework of model-checking LTL-X action-based properties on Petri nets. We propose an incremental and modular verification approach where the system model is partitioned according to the actions occurring in the property to be verified and where the environment of a component is taken into account using the linear place invariants of the system.

Lundi 11 Juin 2007, salle B311 à 15h30 : Stefano Guerrini (Dipartimento di Informatica, Roma La Sapienza).

Title: Commutative Locative Quantifiers for Multiplicative Linear Logic
Abstract: The paper presents a solution to the technical problem posed by Girard after the introduction of Ludics of how to define proof nets with quantifiers that commute with multiplicatives. According to the principles of Ludics, the commuting quantifiers have a ``locative'' nature, in particular, quantified formulas are not defined modulo variable renaming. The solution is given by defining a new correctness criterion for first-order multiplicative proof structures that characterizes the system obtained by adding a congruence implying $\forall x (A \tens B) = \forall x A \tens \forall x B$ to first-order multiplicative linear logic with locative quantifiers. In the conclusions we shall briefly discuss the interpretation of locative quantifiers as storage operators.

Lundi 2 Avril 2007, salle B311 à 15h30 : Luca Saiu (Ing. Recherche LIPN).

Title: An introduction to compiler construction and functional programming through the implementation of GNU epsilon.
Abstract: The problems of realistic functional languages use and implementation will be introduced in the context of 'epsilon', a language implemented by the speaker for the GNU Project and still in flux.
After a practical demonstration presenting functional programming an outline of epsilon across its three major rewrites will follow, with particular emphasis on expressivity, generality and efficiency. A whirlwind tour on the epsilon implementation will lead to a description of the epsilon abstract machine (the "eAM"). The eAM is an extremely general target platform implemented for epsilon but not limited to it in any way: the eAM was thought from the beginning to be suitable as a low-level intermediate language for whatever kind of high-level programming language, with performance comparable to C.
The seminar will close with a glance at the future evolutions of the language, hinting at opportunities and challenges.

Lundi 26 Mars 2007, salle B311 à 15h30 : Paolo Di Giamberardino (Univ. Rome)

Title:Jump from Parallel to Sequential Proofs: Additives
Abstract: We introduce a new class of multiplicative\additive proof nets, J-proof nets, which are a typed version of Faggian and Curien's L-nets. In J-proof nets, we can characterize nets with different degrees of sequentiality, by gradual insertion of sequentiality constraints (jumps). As a byproduct, we obtain a simple proof of the sequentialisation theorem.
Due to the close connection between J-proof nets, L-nets (linear strategies), and event structures (models of concurrency), our sequentialisation method applies in all these domains
Slides : download.

Lundi 12 Mars 2007, salle B311 à 15h30 : Micaela Mayero (LIPN).

Titre : Certification de Programmes d'Analyse Numérique (CerPAN)
Résumé : Je présenterai le projet ANR 2005 CerPAN. L'objectif de ce projet est de développer et mettre en application des méthodes permettant de démontrer formellement la correction de programmes issus du domaine de l'analyse numérique. Beaucoup de programmes critiques sont issus de cette science, mais les travaux traitant directement des applications des méthodes formelles aux programmes d'analyse numérique sont rares. La principale raison est l'utilisation intensive des nombres à virgule flottante dans les programmes numériques, alors que les méthodes formelles manipulent plutôt des nombres entiers, ou plus généralement des structures discètes.
Deux méthodes sont explorées dans ce projet. L'une consiste à utiliser des outils basés sur Why tels que Caduceus. L'autre consiste à effectuer la formalisation et la preuve du problème, puis à utiliser le principe d'extraction du système Coq.
Un autre objectif du projet est également de tenir compte des aspects d'efficacité qui peuvent jouer un rôle déterminant dans le domaine de l'analyse numérique en particulier.

Lundi 19 Février 2007, salle B311 à 15h30 : Martin Hofmann (LMU München - Institut für Informatik).

Titre : Correctness of program transformations with effects and regions (joint work with Nick Benton, Andrew Kennedy, Lennart Beringer)
Résumé : We give a denotational semantics to a region-based effect system tracking reading, writing and allocation in a higher-order language with dynamically allocated integer references. The purpose of the semantics is to validate a number of effect-dependent program equivalences in the sense of observational equivalence. An example is the following:
x=M;y=M;N(x,y) is equivalent to x=M;N(x,x)
provided that M does not read from memory regions that it writes to and moreover does not allocate memory that is encapsulated in the values of x and y. Here x can be a higher-order function or a reference or a combination of both.
The two sides of the above equivalence are related in our denotational semantics and by our adequacy result this implies that they are observationally equivalent, ie can be replaced by one another in any (well-typed) program.

Lundi 12 Février 2007, salle B311 à 15h30 : Jean-Yves Marion (Loria - INPL).

Titre : Recursion Theorem, Information Theory, a theoretical travel in virus land
Résumé : We are concerned with theoretical aspects of computer viruses. For this, we suggest a new definition of viruses which is clearly based on the iteration theorem and above all on Kleene’s recursion theorem. We show that we capture in a natural way previous definitions, and in particular the one of Adleman. We establish generic virus constructions and we illustrate them by various examples. Lastly, we show results on virus detection.

Lundi 29 Janvier 2007, salle B311 à 15h30 : Paul Ruet (IML).

Titre : Dynamique discrète et structure des réseaux de régulation génétique.
Résumé : Les réseaux de régulation génétique sont habituellement représentés par des graphes dirigés signés. Je parlerai de règles proposées par le biologiste René Thomas reliant la structure de ces graphes avec certaines propriétés de leur dynamique. Ces règles prédisent plus précisément que la présence d'un circuit positif est une condition nécessaire à l'existence de plusieurs états stationnaires (c'est-à-dire à la différentiation), et que la présence d'un circuit négatif est une condition nécessaire à l'existence d'oscillations stables (homéostasie). Je présenterai les résultats obtenus dans le cadre d'une dynamique discrète. L'exposé ne supposera aucune connaissance préliminaire.
Slides : download.

Lundi 13 Novembre 2006, salle B311 à 15h30 : Frédéric Gilliers (LIP6).

Titre : Développement orienté modèle de systèmes répartis : L'expérience du projet MORSE.
Résumé : Le projet MORSE est un projet RNTL lancé en 2003, pour une durée de 3 ans. Son objectif est de fournir une méthodologie outillée de développement d'applications réparties asynchrones compatible avec un environnement industriel.
Dans cet exposé, je présenterai donc la méthodologie de développement ainsi que l'outillage développés dans le cadre du projet. Cette méthodologie est basée sur la notation UML pour la représentation des modèles de haut niveau de l'application, Cette spécification est enuite traduite en LfP, un langage de modélisation que nous avons développé. Cette nouvelle spécification permet de vérifier le modèle (par model checking) ainsi que de générer automatiquement une implémentation de la spécification (génération automatique de code).