SÉMINAIRE 2005-06

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.

lundi 12 Juin 2006, salle B311 à 13h30, dans le cadre du groupe de travail NO-CoST : Paolo Coppola (université de Udine) exposé en anglais.

Titre : Elementary type assignment system for call-by-value lambda calculus
Résumé : The so-called light logics [Girard98,Asperti98,Asperti02] have been introduced as logical systems enjoying quite remarkable normalization properties. Designing a type assignment system for pure lambda calculus from these logics, however, is problematic, as discussed in [Baillot04]. Simona Ronchi della Rocca, Ugo Dal Lago and the speaker have shown in a recent paper [TLCA2005] that shifting from usual call-by-name to call-by-value lambda calculus allows regaining strong connections with the underlying logic. This will be done in the context of Elementary Affine Logic, designing a type system in natural deduction style assigning EAL formulae to lambda terms.

lundi 12 Juin 2006, salle B311 à 15h30 : Cosimo Laneve (Université de Bologne) séminaire en anglais.

Titre : Web services foundations and PiDuce
Résumé : I will overview three technologies for Web services: WS-BPEL, WSDL, and WSCL pointing out the basic operations therein. Then I focus on the foundational aspects of such technologies with the aim of providing a formal semantics, a correct implementation, and kit of safe static analyzers. These technologies will be therefore analyzed by means of PiDuce, a process calculus with XML values and datatypes, that have been prototyped at University of Bologna (www.cs.unibo.it/PiDuce).
The talk is not technical and does not require any ad-hoc knowledge. In case some topics are more interesting than others, I will be glad to discuss them in future meetings.

lundi 27 Mars 2006, salle B311 à 15h30 : Sana Hamdoun (ATER Université Paris 13, LIPN) et Mohamed Badri (Université Paris 5)

Titre : Construction et Maintenance des Entrepôts de Données Hétérogènes
Résumé : La construction de gros volumes de données afin de disposer, à tout moment, d’outils d’aide à la décision est devenue, de nos jours, un sujet très important dans le monde industriel. L’abondance des informations et leur hétérogénéité complique la tâche d’intégration de données et leur maintenance au moindre coût. Nous proposerons dans cet exposé un outil d’intégration de données hétérogènes structurées et semi-structurées. Notre méthode est basée sur les liens de synonymie et d’inclusion qui peuvent exister entre les informations à travers les bases de données concernées. Nous proposons, par ailleurs, deux procédures de maintenance de vues matérialisées (VM) issues de données hétérogènes complexes. Notre proposition se base sur une critique du Système de Gestion de Bases de Données Oracle et met en évidence ses limites quant à la gestion des vues matérialisées. Des mesures seront présentées pour comparer les performances.
Slides : download.

lundi 13 Mars 2006, salle B311 à 15h30 : Benoit Valiron (Université d'Ottawa)

Titre : A lambda calculus for quantum computation with classical control
Résumé : We develop a functional programming language for quantum computers, by extending the simply-typed lambda calculus with quantum types and operations. The design of this language adheres to the ``quantum data, classical control'' paradigm, following Peter Selinger's work on quantum flow-charts. We define a call-by-value operational semantics, and we give a type system using affine intuitionistic linear logic. The main results of this work are the safety properties of the language and the development of a type inference algorithm.

lundi 6 Mars 2006, salle B311 à 15h30 : Sebastien Bardin (ATER ENS Cachan, LSV) exposé en anglais

Titre : Theorie et pratique de l'acceleration.
Résumé : Le model checking est maintenant une technique mature pour les systemes a espaces d'etats finis. Cependant, de nombreuses machines reelles ont naturellement un espace d'etats infini. Nous nous interessons a la verification de systemes infinis. Notre approche se base sur :
1) une representation symbolique pour manipuler effectivement des ensembles infinis X d'etats atteignables
2) des algorithmes d'acceleration pour calculer en un pas t^*(X), ou t est un circuit du systeme
3) une heuristique pour selectionner les circuits a accelerer.
Nous montrerons comment cette approche a ete instanciee dans le cas des systemes a compteurs. Les resultats ont ete implantes dans l'outil FAST, qui a permi de verifier a ce jour une 40 de systems a compteurs infinis, et surpasse les outils concurrents de calcul symbolique exact.
Slides : download.

13 février -- 3 mars : pause dans le séminaire en partie due aux workshops de Geocal'06 (Marseille)

lundi 6 Février 2006, salle B311 à 15h30 : Paulin Jacobé de Naurois (ATER Univ. Paris 13 2005-06, LIPN)

Titre : Une Mesure d'Espace pour le Calcul BSS sur les Réels
Résumé : Dans le cadre du modèle BSS de calcul sur les réels, il a été montré que tout problème décidable en temps borné est décidable en espace constant. Des algorithmes numériques naturels, extensions d'algorithmes booléens LOGSPACE, échappent dès lors à une classification satisfaisante en termes de complexité.
Je propose donc une nouvelle mesure de complexité en espace pour le modèle de calcul BSS sur les réels, inspirée du modèle faible de Koiran. Je définis ainsi des classes de complexité en espace, LOGSPACE_W et PSPACE_W. Je prouve que LOGPSACE_W est incluse dans NC2_R et dans P_W, c'est à dire qu'elle est suffisamment petite pour être discriminante. Je prouve également l'existence d'un problème NP_R-complet pour des réductions LOGPSACE_W, c'est à dire que LOGPSACE_W est assez large pour contenir des algorithmes naturels interessants. Je montre également que PSPACE_W est incluse dans PAR_R.
Slides : download.

lundi 9 Janvier 2006, salle B311 à 15h30 : Jean-Yves Moyen (post-doc CNRS 2005-06, LIPN)

Titre : Analyse de programmes et complexité implicite.
Résumé : Je présente ici différentes techniques d'analyses de programmes en vu d'obtenir des bornes sur la complexité. Ces techniques permettent d'analyser des programmes écrits dans un langage fonctionnel du premier ordre et se basent principalement sur la notion d'ordre de terminaison. L'autre outil clé de ces analyses est la notion de quasi-interprétations. J'essaye de présenter un bref aperçu historique des techniques ayant abouti à l'introduction de ces quasi-interprétations.
Ainsi, je présente plusieurs caractérisation syntaxiques de classes de complexité usuelle comme Ptime ou Pspace. De plus, je mets autant que possible l'accent sur les aspects de complexité implicite (complexité du programme comparée à la complexité de la fonction comparée) et d'intentionnalité (capturer le plus possible d'algorithmes "naturels" dans la caractérisation).

lundi 12 Décembre 2005, salle B311 à 15h30 : Emmanuel Beffara (PPS, Université Paris 7)

Titre : Réalisabilité concurrente
Résumé : Dans cet exposé, on développera une technique de réalisabilité permettant la construction de modèles de la logique linéaire à partir de processus concurrents. On utilise pour cela une variante du pi-calcul, munie d'une notion paramétrable d'observation (divergence, may- ou must-testing...), d'où l'on déduit une notion abstraite de comportement. La structure de ces comportements mène à la définition de connecteurs logiques, inspirés des logiques spatiales et temporelles, qui décrivent les propriétés fondamentales des processus. Le système obtenu est une forme de logique linéaire qui définit pour le pi-calcul un système de type qui garantit des bonnes propriétés comme la terminaison et l'absence de blocage. D'autre part, ce système de type établit une correspondance à la Curry-Howard entre la concurrence et diversesvariantes de logique linéaire, qui s'intègre bien aux précédentes études sur la décomposition du calcul fonctionnel dans les calculs concurrents.
Slides : download.

lundi 28 novembre 2005, salle B311 à 15h30 : Ugo Dal Lago (Dipartimento di Scienze dell'Informazione, Università degli Studi di Bologna) séminaire en anglais.

Titre : An Invariant Cost Model for the Lambda Calculus
Résumé : We define a new cost model for the call-by-value lambda-calculus satisfying the invariance thesis. That is, under the proposed cost model, Turing machines and the call-by-value lambda-calculus can simulate each other within a polynomial time overhead. The model only relies on combinatorial properties of usual beta-reduction, without any reference to a specific machine or evaluator. In particular, the cost of a single beta reduction is proportional to the difference between the size of the redex and the size of the reduct. In this way, the total cost of normalizing a lambda term will take into account the size of all intermediate results (as well as the number of steps to normal form).
Slides : download.

lundi 21 novembre 2005, salle B311 à 15h30 : Jean-Yves Girard (Institut de Mathématiques de Luminy, Marseille)

Titre : GdI DANS LES ALGEBRES DE v NEUMANN
Résumé : Une algèbre de vN est FINIE quand uu* = 0 implique u*u = 0 ; autrement dit quand elle a une TRACE. L'exemple standard est fourni par l'algèbre de convolution d'un groupe discret. Quand toutes les classes de conjugaison sont infinies, on obtient même un FACTEUR (algèbre connexe) ; il a une trace unique, qui permet de définir univoquement la DIMENSION 0 \le dim(E) \le 1 de tout sous-espace, toutes les valeurs étant prises : on parle de facteur de type II_1. Une autre hypothèse est l'HYPERFINITUDE (sans rapport à la finitude), qui dit que l'algèbre est approximable par des matrices finies à coefficients complexes, mais de taille variable ; ce qui est le cas quand le groupe discret est une union filtrante de groupes finis. Un célèbre théorème de Murray-vNeumann dit qu'il n'y a qu'un seul facteur hyperfini de type II_1 (i.e., fini non trivial).
C'est dans ce facteur que je veux récrire la GdI pour obtenir "la" bonne logique ICONOCLASTE, i.e., la variante correcte de la galaxie LLL. Grosso modo, on a une algèbre infinie, mais modérément infinie : ainsi les p,q de la GdI sont absents (puisque p*p=1, alors que pp*\neq 1, ce qui est précisément ce qui s'oppose à la trace). La plus grosse part de l'infini est externe, et seul un petit morceau subsiste à l'intérieur. Le système logique qui s'interprétera dans ce cadre sera forcément très modéré quant à l'infini.

lundi 17 octobre 2005, Amphi. Euler à 15h30 : Claudia Faggian (Dipartimento di Matematica Pura ed Applicata, Universita' degli Studi di Padova)

Titre : L-nets, parallel strategies and proof-nets
Résumé : We present L-nets as a game model allowing for concurrent interaction. L-nets have been developed in the context of Ludics (Girard 2001), which can be seen as a game model of sequential interaction, abstracting away from proof-theory. The talk will focus on L-nets as parallel strategies (in standard game-semantical terms) and as an abstract form of MALL proof nets.
Strategies capturing sequential interaction, such as Hyland-Ong innocent strategies or Girard's designs, are based on trees; during an interaction (play, or run) the order between the actions is totally specified. L-nets on the contrary are based on graphs, and interactions are partial orders; the intuitionis that some actions can be performed in parallel (or scheduled in any order), while there are tasks which depend upon other tasks.
When taking a proof-theoretical point of view, a tree strategy can be seen as an abstract sequent calculus derivations, while an L-net appears as an abstract (multiplicative-additive) proof-net. Moreover, as a tree strategy is a particular case of L-net, we have a homogeneus setting, in which it is possible to move between different degrees of sequentiality.
This talk is based on work in collaboration with Francois Maurel and with Pierre-Louis Curien.

lundi 3 octobre 2005, salle B311 à 15h30 : Kazushige Terui (National Institute of Informatics, Tokyo)

Titre : Towards a semantic characterization of cut-elimination (joint work with Agata Ciabattoni)
Résumé : A huge number of logics and sequent calculi have been invented in the literature. Among them, some enjoy cut-elimination, but the others do not.
In this talk, we consider a class of "simple" sequent calculi, each defined by a set of structural and logical inference rules, and give a necessary and sufficient condition for such a calculus to admit cut-elimination in terms of phase semantics.
Our condition is partly due to Girard's naturality condition for logical principles (Girard 1999). The other part is obtained by an analysis of Okada's phase-semantic proof of cut-elimination for Linear Logic.
Slides : download. The final version of the journal paper is also available.