4th Project meeting, May 26 2010, Univ. Paris 13

4th Project Meeting of COMPLICE: Wednesday May 26 2010, University Paris 13, LIPN.

Access: University Paris 13, amphithéatre Copernic de l’institut Galilée (G on the following map http://www-lipn.univ-paris13.fr/pla...)

Programme

Résumés

 Titre : La logique linéaire élémentaire revisitée. Patrick Baillot (LIP, ENS Lyon)

Résumé : Dans cet exposé je considérerai la logique linéaire élémentaire avec points fixes de types et je donnerai une caractérisation dans ce système des classes P et EXP.

 Titre: Interpretation of Stream Programs. Romain Péchoux (CARTE, Nancy 2)

Résumé : The lazy functional languages are useful in order to deal elegantly with infinite data structures, including streams, as primitive data types. Moreover, the functional setting offer tools and techniques that can be used in the analysis of stream programs properties. In this presentation we describe a general methodology built on (quasi and sup) interpretation-based techniques that can be used to analyze the memory space of stream functional programs. This techniques have been developed in order to prove some stream programs space properties and some input-output size relations about stream progams.

 Titre : Plongement des types intersection dans IMLL. Jean-Marie Madiot (stagiaire M1, ENS Lyon)

Résumé : Les types intersection présentent l’intérêt de caractériser les termes normalisables du lambda calcul. On peut mettre en relation la logique intuitionniste NJ avec les types intersection avec intersection idempotente (DΩ). Ici on s’intéresse à une logique induite par une version sans idempotence, qu’on met en relation avec le fragment intuitionniste de la logique linéaire multiplicative, IMLL. On étudie la normalisation de tête en tentant d’assurer un système complet - c’est à dire typant tous les termes normalisants - mais aussi correct - c’est à dire respectant des propriétés de réduction et d’expansion du sujet, ou établissant un lien avec les coupures de la logique sous-jacente.

 Titre: Distinctions de classes par "course-of-value". Guillaume Bonfante (LORIA)

Résumé: Ce travail rentre dans le cadre d’une analyse des algorithmes couverts par certaines théories calculatoires. Nous nous intéressons à des transformations qui permettent de distinguer les ensembles de programmes. Nous présentons la transformation "course-of-value" (cov) et nous montrons que : cov+cons-free = PTIME, cov+interpretation = PTIME, cov+PPO+sous-terme = PTIME, et cov+PPO+embedding=PSPACE.

 Titre : Implémentation de la méthode mwp et plus si affinité. Jean-Yves Moyen (LIPN, Univ. Paris 13)

Résumé : La méthode mwp a été développée par L. Kristiansen et N. D. Jones. Elle permet d’analyser des programmes impératifs simple (langage LOOP qui ne contient que des boucles for) pour détecter ceux qui terminent en temps polynomial. Cette méthode a été améliorée ensuite par L. Kristiansen et A. Ben-Amram : au prix d’une non-déterminisation du langage, on obtient une méthode qui est décidable et *intensionellement complète* pour Ptime. Bien sûr, l’indécidabilité reste présente lors de la transformation d’un "vrai" programme dans le langage étudié. Je présenterai une implémentation de la méthode mwp et, peut-être, de son extension.