Rencontre annuelle GeoCal, 15 février 2013
Rencontre annuelle du groupe de travail <a href="http://iml.univ-mrs.fr/~regnier/gdr-im/">Géométrie du Calcul (GeoCal)</a> du <a href="http://www.gdr-im.fr/">GDR Informatique Mathématique</a>
Lieu
La rencontre aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, en amphi B le matin, en salle des examens l'après-midi. Pour venir, voir les instructions sur le site du LIP ou sur un plan, par exemple chez Google Maps. À l'entrée, se présenter à la réception, qui aura la liste des inscrits.
Programme
- 10:30 – 11:00
-
Pierre-Louis Curien (CNRS)
(travail en commun avec Richard Garner (Macquarie University, Sydney) et Martin Hofmann (Ludwig-Maximilian's-Universität, München)
We relate Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian closed categories. As an outcome, we obtain a new proof of the coherence theorem that Curien had proved, which implied that Seely's interpretation in the end was sound.
(exposé en français)
- 11:00 – 11:30
-
Flavien Breuvart (Université Paris Diderot)
Il existe une vaste littérature traitant de résultats d'adéquation complète (c'est à dire la correspondance entre la congruence dénotationnelle et la congruence observationnelle) pour une multitude de couple modèle-langage. Mais l'adéquation complète en tant qu'objet a rarement été étudiée, à l'exception notable du langage PCF, pour lequel Milner a caractérisé la classe des modèles complétement adéquats, qui sont ceux dont les éléments compacts sont définissables. Même dans le cas du lambda-calcul, s'il existe des conditions nécessaires (extensionnalité) ou suffisantes (stratification), aucune caractérisation n'a été donnée. Je vais donc expliquer comment, dans une classe de modèle suffisamment restreinte, la caractérisation de l'adéquation complète pour le lambda-calcul se trouve être surprenamment complexe.
- 12:00 – 12:30
-
Yves Lafont (Université d'Aix-Marseille) et Pierre Rannou (Université d'Aix-Marseille)
La réécriture de diagrammes, inspirée par les travaux d'Albert Burroni sur les catégories monoïdales, généralise à la fois la réécriture de mots (pour les monoïdes) et la réécriture de termes (pour les théories algébriques du premier ordre). La confluence et la terminaison de tels systèmes de réécriture ont d'abord été étudiées par Yves Lafont, puis Yves Guiraud, notamment dans le cadre de l'algèbre linéaire sur le corps fini à 2 éléments. Une généralisation de ce calcul pour un corps K quelconque, apparentée au calcul matriciel, a été étudiée par Pierre Rannou.
- 14:00 – 14:30
-
Jean-Baptiste Midez (Université d'Aix-Marseille)
- 14:30 – 15:00
-
Paul-André Melliès (CNRS)
Dans cet exposé, j'expliquerai comment utiliser le principe de chiralité pour décomposer la négation tensorielle en constituants élémentaires. L'analyse débouchera sur une présentation purement combinatoire de la notion de catégorie de dialogue. Les combinateurs que j'obtiens sont les suivants: (1) une négation involutive, (2) une adjonction entre foncteurs de contrôle L et R, (3) une paire de combinateurs axiome - coupure, et (4) une paire de lois distributives en chiralité. J'expliquerai au moyen de diagrammes de cordes comment chacun de ces combinateurs raffine le combinateur lui correspondant en logique linéaire. Mon exposé s'appuiera en grande partie sur les <a href="http://www.pps.univ-paris-diderot.fr/~mellies/tensorial-logic.html">articles 4 et 5</a> que je viens de mettre en ligne.
- 15:30 – 16:00
-
Thomas Seiller (INRIA)
Suite à son travail récent utilisant des algèbres de von Neumann, Girard a proposé une nouvelle approche pour l'étude des classes de complexité. Cette méthode utilise la construction du produit croisé entre une algèbre et un groupe agissant sur celle-ci. Cette construction consiste à internaliser les automorphismes externes représentés par le groupe, et Girard propose de caractériser les classes de complexité par des ensembles d'opérateurs engendrés par ces internalisations.
Nous avons étudié, avec Clément Aubert, le cas de l'action du groupe des permutations des entiers naturels sur un produit tensoriel. Dans un premier travail, nous avons montré que dans ce cas la méthode proposée par Girard permet d'obtenir une caractérisation de la classe co-NL (le complémentaire de l'ensemble des langages décidables par une machine de Turing non-déterministe en espace logarithmique). Afin de prouver ce résultat, nous avons défini la notion de machine à pointeurs qui s'avère être une nouvelle caractérisation de co-NL par des machines abstraites. Plus récemment, nous avons étendu ce travail en définissant un ensemble d'opérateurs caractérisant exactement la classe L (LogSpace).
