Institut de Mathématiques de Luminy

SÉMINAIRES 2011
Logique et Interactions

Organisateur :
Emmanuel Beffara (tél. 04 91 26 96 35)
Lieu : IML, Bâtiment TPR2- CNRS :
Salle de Séminaires : 3ème étage (304-306).
Horaire : en règle générale le jeudi, à 14h.


Thomas Seiller

jeudi 1er décembre
Thomas Seiller
(LAMA, Chambéry) :
Graphes d'interaction

Webpage : http://iml.univ-mrs.fr/~seiller/

Résumé : Les graphes d'interaction généralisent la toute première géométrie de l'interaction définie par Girard dans l'article “Multiplicatives”. En remplaçant les permutations (utilisées dans “Multiplicatives”) par des graphes orientés pondérés, il est possible de définir une notion d'orthogonalité en comptant les cycles apparaissant lors du branchement de deux graphes. Il est alors possible d'obtenir une géométrie de l'interaction pour MALL dépendant de la fonction qui mesure les cycles. Après avoir défini cette géométrie de l'interaction, je montrerai comment il est possible d'obtenir un modèle dénotationnel de MALL et une notion de vérité à partir de ce modèle. Enfin, je montrerai qu'en choisissant judicieusement la fonction de mesure, il est possible d'obtenir soit la géométrie de l'interaction dans sa version ancienne (GdI1, avec une orthogonalité basée sur la nilpotence), soit une version combinatoire de la GdI5 de Girard. Ceci permet donc de donner une interprétation géométrique à l'orthogonalité de Girard basée sur le déterminant, et de relier cette nouvelle construction à celles plus anciennes basées sur la nilpotence.


Patrick Baillot

jeudi 17 novembre
Patrick Baillot
(LIP, ENS Lyon) :
La logique linéaire élémentaire revisitée :
temps polynomial et hiérarchie de classes de temps exponentiel

Webpage : http://perso.ens-lyon.fr/patrick.baillot/

Résumé : Les variantes de la logique linéaire pour la complexité implicite, comme ELL, LLL, SLL, ont permis de caractériser plusieurs classes de complexité: P, la classe Elem du temps élémentaire (tour d'exponentielles de hauteur bornée), PSPACE? Dans ces différents systèmes les modalités exponentielles sont définies par des règles plus ou moins faibles, qui limitent le pouvoir d'expression de la logique. Les comparaisons des systèmes entre eux restent cependant difficiles.
Nous proposons une autre démarche consistant à caractériser dans une même logique plusieurs classes de complexité, en considérant pour chacune un type différent. Pour cela nous nous intéressons à la logique linéaire élémentaire ELL, introduite par Girard, un sous-système simple de la logique linéaire permettant initialement de caractériser la classe Elem. Nous considérons son extension avec des points fixes de types et montrons que malgré sa simplicité, cette logique permet de caractériser la classe P et les différents niveaux d'une hiérarchie de classes de complexité de temps exponentiel.


Victor Chepoi

jeudi 27 octobre
Victor Chepoi
(LIF, Marseille) :
Nice labeling of event structures and embedding
of CAT(0) cube complexes into products of trees

Webpage : http://pageperso.lif.univ-mrs.fr/~victor.chepoi/

Abstract: In this talk, we present a counterexample to a conjecture of Rozoy and Thiagarajan from 1991 (called also the nice labeling problem) asserting that any (coherent) event structure with finite degree admits a labeling with a finite number of labels, or equivalently, that there exists a function f : N → N such that an event structure with degree ≤ n admits a labeling with at most f(n) labels. Our counterexample is based on the Burling’s construction from 1965 of 3-dimensional box hypergraphs with clique number 2 and arbitrarily large chromatic numbers and the bijection between domains of event structures and median graphs (alias 1-skeletons of CAT(0) cube complexes) established by Barthélemy and Constantin in 1993.
In the second part of the talk, we will outline the proof that the contact graph of a 2-dimensional CAT(0) cube complex X of maximum degree d can be coloured with at most q(d)= Md^15 colours, for a fixed constant M. This implies that X (and the associated median graph) isometrically embeds in the Cartesian product of at most q(d) trees, and that the event structure whose domain is X admits a nice labeling with q(d) labels. This second result is based on a join paper with Mark Hagen.


Pierre Hyvernat

jeudi 29 septembre
Pierre Hyvernat
(LAMA, Chambéry) :
Foncteurs polynomiaux,
jeux et logique linéaire (différentielle)

Webpage : http://www.lama.univ-savoie.fr/~hyvernat/


jeudi 15 septembre
Barbara Petit
(LIP, ENS Lyon)
Sémantique du lambda-calcul avec constructeurs

Webpage : http://perso.ens-lyon.fr/barbara.petit/

Résumé : Le lambda-calcul avec constructeurs est une extension du lambda-calcul avec un mécanisme de filtrage (pattern matching). Le filtrage à la ML y est décomposé en deux étapes: une simple analyse de cas sur des constantes, et une règle surprenante de commutation entre l'application et la construction de filtrage.
Dans cet exposé, nous définirons une notion générique de modèle catégorique pour ce calcul. Nous construirons ensuite un modèle particulier, le modèle syntaxique (dans la catégorie des PERs), et nous en déduirons un résultat de complétude.
Enfin nous montrerons comment construire des modèles non syntaxiques du lambda-calcul avec constructeurs en partant d'une traduction CPS. On obtiendra ainsi des modèles par continuation pour le calcul.


logo LIPN

mardi 5 juillet
Beniamino Accattoli
(LIPN, Villetaneuse)
The kingdom of polarity and the polarity of the kingdom

Webpage : https://sites.google.com/site/beniaminoaccattoli/

Abstract: The aim of the talk is to present a study on a local and implicit notion of box for Linear Logic Proof-Nets, i.e., a notion of box which is not given, but induced by correctness and enjoying a local algorithm for its reconstruction. We start by showing that in Multiplicative Linear Logic there is no hope of obtaining such a notion, and so Linear Logic Proof-Nets cannot admit local implicit boxes. We then show that in a certain polarized setting, it is possible to decorate the net with some additional edges, called jumps, so that the smallest subnet having as conclusion a given positive formula P, called the kingdom of P, admits a local and implicit definition. Then we show a mismatch between polarity inducing implicit boxes and polarity as in Polarized Linear Logic. If time permits, we shall conclude by showing that the new box-free formalism - having a slightly different operational semantics than ordinary proof-nets - admits a simple and direct proof of strong normalization, not using the usual schema of proving Weak-Normalization plus a conservation theorem.


Daniel de Carvalho

jeudi 30 juin
Daniel de Carvalho
(LIPN, Villetaneuse)
Injectivité de la sémantique relationnelle
pour la logique linéaire

Webpage : http://www-lipn.univ-paris13.fr/~decarvalho/



jeudi 23 juin
à 1
0h
Dimitri Ara
(IMJ, Paris 7)
Modèles homotopiques de la théorie des types

Webpage : http://www.normalesup.org/~ara/index.html


jeudi 19 mai
Stéphane Zimmermann
(PPS, Paris 7)
Connecteurs synthétiques
en logique linéaire différentielle

Webpage : http://www.pps.jussieu.fr/~zimmerma/


Peter Selinger

lundi 28 mars et jeudi 31 mars
Peter Selinger
(Dalhousie, Canada)
Logical approaches to quantum information theory

Webpage : http://www.mscs.dal.ca/~selinger/

Abstract: These lectures will be a re-run of similar lectures I gave at Paris 13 in February. I'll start with a brief introduction to quantum computing. There are many formulations of quantum physics, but one that is particularly suitable for a logical treatment is the formulation in terms of density matrices and completely positive maps. This will tie in with C^*-algebras, and more generally, with dagger compact closed categories. I'll talk about the importance of higher-order functions in quantum computations. In fact, I will argue that most, if not all, interesting quantum phenomena occur at higher-order types. Finally, I'll talk about the quantum lambda calculus. Its type system is given by a very slight modification of intuitionistic linear logic.


Clément Aubert

jeudi 24 mars
Clément Aubert
(LIPN, Villetaneuse) :
Réseaux de preuve booléens uniformes
sous-logarithmiques


Webpage: http://www-lipn.univ-paris13.fr/~aubert/


jeudi 10 mars
Sergeï Lenglet
(Univ. Wroclaw, Pologne) :
Expansion for universal quantifiers


Webpage: http://sardes.inrialpes.fr/~slenglet/

Abstract: Expansion is a tranformation on typings (i.e. on pairs typing environment - result types) used in intersection types to deduce a typing from an other one (usually from a principal typing). The definition of this operation has been made easier by the introduction of expansion variables by Carlier and Wells in System E. In this talk, we present System Fs, an extension of system F with expansion variables. We explain how we introduce expansion in a type system with universal quantifiers, present the main differences between the expansion in System E and in System Fs, and give the benefits of this operation in terms of type inference.


Alexandre Miquel

jeudi 24 février
Alexandre Miquel
(LIP, ENS Lyon) :
Une analyse calculatoire de la transformation
de preuve par forcing

Webpage : http://perso.ens-lyon.fr/alexandre.miquel/

Résumé : Le forcing est une technique inventée par Cohen pour démontrer la cohérence et/ou l'indépendance de certains axiomes vis-à-vis de la théorie des ensembles. Du point de vue de la théorie de la démonstration, le forcing repose sur une traduction des formules et des preuves paramétrée par un ensemble ordonné quelconque : l'ensemble des "conditions de forcing". Récemment, Krivine a proposé une méthode permettant de combiner le forcing avec la théorie de la réalisabilité classique, et a montré que la traduction des preuves par forcing correspond (au niveau des termes de preuves à la Curry) à une transformation de programme étonamment compréhensible.
Suite aux travaux de Krivine, je montrerai comment reformuler le forcing en arithmétique d'ordre supérieur, en me plaçant dans une extension adéquate du système F-omega (classique) avec termes de preuves à la Curry. Je présenterai la traduction des formules et la transformation de preuve-programme sous-jacente. Enfin, j'analyserai le comportement calculatoire des programmes traduits, et en déduirai une extension de la machine de Krivine avec environnements explicites - la KFAM - conçue pour traiter directement les preuves par forcing sans passer par la transformation de programme. Je concluerai sur les liens que cette étude fait apparaître entre la méthode de forcing et certains principes à la base des systèmes d'exploitation, ainsi que sur les perspectives en logique.


Tom Hirschowitz

jeudi 3 février
Tom Hirschowitz
(LAMA, Chambéry) :
Une ludique pour CCS?


Webpage : http://www.lama.univ-savoie.fr/~hirschowitz/

Résumé : Au début, on voulait faire un début de ludique pour CCS, dans le sens une semantique de jeux, pour laquelle on définit une notion d'équivalence observationnelle par orthogonalité. Mais CCS est un langage concurrent, donc la notion habituelle de stratégie est trop grossière. Du coup, l'approche proposée est à mi-chemin entre la ludique et les travaux de Joyal, Nielsen et Winskel sur les préfaisceaux comme modèles de la concurrence. On va même plus loin que les préfaisceaux, puisque la notion d'innocence est interprétée comme une condition de faisceau, pour une topologie adéquate. On montre ensuite que nos stratégies forment un champ, dans lequel le recollement de deux stratégies s'interprète comme leur interaction. Grâce à ça, on définit une notion générale de critère d'observation (sans doute pas dans sa forme finale), chaque critère induisant par orthogonalité une notion d'équivalence. On considère enfin deux instances concrètes, correspondant respectivement au “fair" et au “must" testing, dont on montre qu'elles coïncident (alors qu'elles diffèrent dans le cadre habituel).Travail en collaboration avec Damien Pous (INRIA Grenoble).


Pierre Hyvernat

vendredi 28 janvier
Pierre Hyvernat
(LAMA, Chambéry) :
Le principe du “size-change termination”
pour les langages avec constructeurs

Webpage : http://www.lama.univ-savoie.fr/~hyvernat/

Résumé : Le size-change termination principle est un test (correct mais forcément incomplet) pour décider la terminaison de programmes mutuellement récursifs. Ce test, dû à A. ben Amram, N.D. Jones et C.S. Lee est particulièrement simple et élégant, tout en étant relativement puissant et modulaire. Il s'agit essentiellement d'une opération de clôture transitive sur le graphe d'appels des fonctions et la preuve de correction repose sur le théorème de Ramsey infini.
Quand le langage des définitions récursives est un langage avec constructeurs / destructeurs à la ML, il y a une notion naturelle de taille : le nombre de constructeurs dans une valeur. Dans ce contexte, on peut généraliser le test pour conserver plus d'information que la seule taille des arguments. Ceci permet notamment d'ignorer certains chemins du graphe d'appels qui ne correspondent à aucune suite concrète d'appels. Par contre, la preuve de correction du nouveau principe est plus complexe que l'originale.
Après une rapide présentation du test original, je décrirais cette extension et donnerai certaines idées de la preuve de correction. Comme le test est implanté (en Caml) pour le langage PML, je donnerais également des exemples (et “contre exemples”) pour permettre de se faire une idée des définitions acceptées (et refusées).


Liste des séminaires de l'année ...
[2002] [2003] [2004] [2005] [2006] [2007] [2008] [2009] [2010]

EL, le 24 novembre 2011