Les séminaires sont communs avec l'équipe Plume (ENS Lyon) et ont lieu en salle de séminaire, premier étage du bâtiment Le Chablais, sur le site du Bourget du Lac ou à l'ENS Lyon.

Prochain séminaire :

Jeudi 23 octobre 2014 à 10h Jacques-Olivier Lachaud (LAMA),
Multigrid-convergence of digital curvature estimators

Résumé : (Masquer les résumés)
Many methods have been proposed to estimate differential geometric quantities like curvature on discrete data. A common characteristics is that they require (at least) one user-given scale parameter, that smooths data to take care of both the sampling rate and possible perturbations. Digital shapes are specific discrete approximation of Euclidean shapes, which come from their digitization at a given grid step. They are thus subsets of the digital plane Z^d. A digital geometric estimator is called multigrid convergent whenever the estimated quantity tends towards the expected geometric quantity as the grid step gets finer and finer. The problem is then: can we define curvature estimators that are multigrid convergent without such user-given parameter ? If so, what speed of convergence can we achieve ? We present here three digital curvature estimators that aim at this objective: a first one based on maximal digital circular arc, a second one using a global optimisation procedure, a third one that is a digital counterpart to integral invariants and that works on 2D and 3D shapes.

Le séminaire de l’équipe LIMD est sous la responsabilité de Xavier Provencal.
Options : Voir par date croissante . Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2015, toutes ensemble.

Année 2014

Jeudi 04 décembre 2014 à 10h30, ENS Lyon TBA (TBA),
Séminaire Chocola

Jeudi 13 novembre 2014 à 10h30, ENS Lyon TBA (TBA),
Séminaire Chocola

Jeudi 06 novembre 2014 à 10h Louis Cuel (LAMA),
À venir

Résumé : (Masquer les résumés)
À venir

Jeudi 23 octobre 2014 à 10h Jacques-Olivier Lachaud (LAMA),
Multigrid-convergence of digital curvature estimators

Résumé : (Masquer les résumés)
Many methods have been proposed to estimate differential geometric quantities like curvature on discrete data. A common characteristics is that they require (at least) one user-given scale parameter, that smooths data to take care of both the sampling rate and possible perturbations. Digital shapes are specific discrete approximation of Euclidean shapes, which come from their digitization at a given grid step. They are thus subsets of the digital plane Z^d. A digital geometric estimator is called multigrid convergent whenever the estimated quantity tends towards the expected geometric quantity as the grid step gets finer and finer. The problem is then: can we define curvature estimators that are multigrid convergent without such user-given parameter ? If so, what speed of convergence can we achieve ? We present here three digital curvature estimators that aim at this objective: a first one based on maximal digital circular arc, a second one using a global optimisation procedure, a third one that is a digital counterpart to integral invariants and that works on 2D and 3D shapes.

Jeudi 16 octobre 2014 à 10h30, ENS Lyon Breuvart Jacobé de Naurois Schmitz (Paris 7, Paris 13, Cachan),
Séminaire Chocola

Jeudi 09 octobre 2014 à 10h Thomas Seiller (Institut des Hautes Études Scientifiques),
Des invariants de cohomologie pour la complexité?

Résumé : (Masquer les résumés)
Je parlerai d'un travail récent qui se trouve à l'intersection entre la logique et la complexité algorithmique. Depuis plusieurs années, de nombreux systèmes logiques capturant des classes de complexité ont été étudiés, certains obtenus comme des systèmes dérivés de la logique linéaire de Girard -- les logiques linéaires bornées. En étudiant des modèles mathématiques de logiques linéaires bornées, on peut montrer une correspondance entre une hiérarchie de classes de complexité et une hiérarchie d'objets mathématiques -- les graphages. Ce résultat ouvre la porte à l'utilisation d'invariants de cohomologie définis sur les graphages en complexité.

Jeudi 02 octobre 2014 à 10h Clovis Eberhart (ENS Cachan),
Semrings, Partial Rings, and Weighted Language Equivalence

Résumé : (Masquer les résumés)
Weighted automata are a structure that has many applications in computer science (speech recognition, natural language processing, image processing, quantitative modelling, etc). Weighted language equivalence is one possible semantics for these weighted automata. This equivalence is decidable for automata with weights on a field, but the proof relies heavily on the properties of fields. However, weighted automata can be defined more generally on a semiring, or even on structures where the addition is defined only partially. This talk explains how the result of decidability for weighted language equivalence for automata on fields can be extended to a decidability result for a certain class of semirings and ``partial semirings''.

Jeudi 25 septembre 2014 à 10h30, ENS Lyon Dal Lago. Schöpp. Vignudelli (Bologne, Munich, Bologne),
Séminaire Chocola

Jeudi 04 septembre 2014 à 10h Flavien Breuvart (PPS),
De la caractérisation des modèles de H*

Résumé : (Masquer les résumés)
Je ferai une présentation rallongée de l'article LICS du même nom. Il s'agit de donner une caractérisation, pour une classe importante de modèles du lambda-calcul non typé, de la pleine adéquation pour la normalisation de tête (i.e. pour H*). On montrera en effet qu'il est pour cela nécessaire et suffisant d'être hyperimmune. L'hyperimmunité est une notion que nous introduirons qui demande à ce que les comportements mal fondés du modèle ne soient pas capturables par des fonctions récursives. Ce résultat sera notamment utilisé comme prétexte et exemple pour l'introduction d'un outil central dans ma thèse: les lambda-calculs avec tests. Il s'agit d'enrichir le lambda-calcul non typé avec des opérateurs directement issus du modèle dénotationnel impliqué afin de rendre celui-ci pleinement adéquat pour notre nouvelle syntaxe. Intuitivement, ces opérateurs vont internaliser un processus d'inférence de type possiblement divergent qui tente de typer l'arbre de Böhm d'un terme.``

Jeudi 26 juin 2014 à 10h Sébastien Labbé (LIAFA),
A d-dimensional extension of Christoffel words

Résumé : (Masquer les résumés)
We extend the definition of Christoffel words to directed subgraphs of the hypercubic lattice in arbitrary dimension that we call Christoffel graphs. Christoffel graphs when d=2 correspond to well-known Christoffel words. Due to periodicity, the d-dimensional Christoffel graph can be embedded in a (d−1)-torus (a parallelogram when d=3). We show that Christoffel graphs have similar properties to those of Christoffel words: symmetry of their central part and conjugation with their reversal. Our main result extends Pirillo's theorem (characterization of Christoffel words which asserts that a word amb is a Christoffel word if and only if it is conjugate to bma) in arbitrary dimension. In the generalization, the map amb↦bma is seen as a flip operation on graphs embedded in ℤd and the conjugation is a translation. We show that a fully periodic subgraph of the hypercubic lattice is a translate of its flip if and only if it is a Christoffel graph.

Jeudi 19 juin 2014 à 10h Clément Aubert (Luminy),
Programmation logique, unification et espace logarithmique

Résumé : (Masquer les résumés)
Nous présentons une construction algébrique qui a pour loi de composition l’unification de termes du premier ordre, et comment y représenter le calcul. La correspondance preuve-programme fournit alors une façon innovante de représenter les entiers binaires comme des fonctions dialoguant avec les programmes. Les machines abstraites que l’on peut y encoder (les observations) peuvent naturellement être vues comme des machines à pointeurs, qui parcourent l’entrée sans la modifier. On montre alors que ces observations sont suffisamment expressives pour caractériser l’espace logarithmique, et que décider de l’acceptation d’un mot par une observation est réductible au problème d’acyclicité d’un graphe, un problème également en espace logarithmique. (En collaboration avec Marc Bagnol [http://iml.univ-mrs.fr/ bagnol/], Paolo Pistone et Thomas Seiller [http://www.ihes.fr/ seiller/])

Jeudi 22 mai 2014 à 10h Karim Nour (LAMA),
Autour de la propriété de l'image(d'un terme) pour la théorie H

Résumé : (Masquer les résumés)
La ``range property'' a été conjecturée par Böhm en 1968 et a résisté 16 ans avant d'être prouvée pour quelques théories du $lambda$-calcul. En 2007, A. Polonsky a montré que la conjecture est fausse pour la théorie $H$. Je présenterai dans cet exposé des conditions nécessaires pour que cette propriété soit vraie pour la théorie $H$. Je donnerai ensuite quelques pistes pour des extensions de ces résultats à d'autres systèmes.

Jeudi 15 mai 2014 à 10h Fabio Zanasi (ENS Lyon),
How to kill epsilons with a dagger - a coalgebraic take on systems with algebraic label structure

Résumé : (Masquer les résumés)
We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or $epsilon$-transitions. Our approach employs monads with a parametrized fixpoint operator $dagger$ to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems. This is joint work with Filippo Bonchi, Stefan Milius and Alexandra Silva.

Mardi 15 avril 2014 à 14h Keiko Nakata (Tallinn University of Technology),
Walking through infinite trees with mixed induction and coinduction: A Proof Pearl with the Fan Theorem and Bar Induction.

Résumé : (Masquer les résumés)
We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of ``eventually always blueness '' and mixed inductive-coinductive ``almost always blueness'' and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction).

Joint work with Marc Bezem and Tarmo Uustalu.

Jeudi 03 avril 2014 à 13h30 Julien Leroy (Université du Luxembourg),
Caractérisation S-adique des sous-shifts minimaux de complexité inférieur à 2n+1

Résumé : (Masquer les résumés)
Généralisant les systèmes dynamiques symboliques substitutifs, un système est dit $S$-adique si son langage est obtenue par itérations successives de substitutions appartenant à l'ensemble fini $S$. La suite de substitutions itérées en est alors une représentation $S$-adique et fournit des informations sur le système (minimalité, nombre de mesures ergodiques, fréquence des lettres,...). Dans cet exposé, je développerai une méthode basée sur les graphes de Rauzy et les mots de retour permettant de construire une représentation $S$-adique ``canonique''. Dans le cas des sous-shifts minimaux dont la différence première de complexité en facteur est majorée par 2 (contenant notamment les sous-shifts sturmiens, d'Arnoux-Rauzy ainsi que les codages de rotations et d'échange de 3 intervales), cette méthode fournit une caractérisation $S$-adique, où $S$ contient 5 substitutions. En particulier, cette caractérisation répond à la conjecture $S$-adique pour ce cas particulier.

Jeudi 20 mars 2014 à 10h Isar Stubbe (Université du Littoral-Côte d'Opale),
Eléments locaux, métriques partiels, diagonaux, et changement de base

Résumé : (Masquer les résumés)
Quelle structure algébrique généralise à la fois les ensembles ordonnés et les espaces métriques? La structure de catégorie enrichie dans une catégorie monoïdale $mathcal{V}$, comme l'a montré Lawvere [1973]. En effet, si on pose $(mathcal{V},otimes,I)=([0,infty]^{sf op},+,0)$, alors la théorie des $mathcal{V}$-catégories est celle des espaces métriques; et si on pose $(mathcal{V},otimes,I)=({0,1},wedge,1)$, alors la théorie des $mathcal{V}$-catégories est celle des ensembles ordonnés. Mais comment faire si on veut parler des {em ensembles ordonnés d'éléments locaux}, autrement dit, des ensembles ordonnés ``dont les éléments ne sont pas définis partout''? Ou, dans le même esprit, si on veut parler des {em espaces métriques partiels}, c'est à dire, des espaces métriques ``dans lesquels la distance d'un point à lui-même n'est pas nécessairement zéro''? Je vais expliquer que, dans ces cas aussi, la structure recherchée est celle de catégorie enrichie---mais, cette fois, enrichie dans une bicatégorie $mathcal{W}$. De plus, pour les éléments locaux comme pour les métriques partiels, la bicatégorie $mathcal{W}$ en question est obtenue par une construction universelle sur une catégorie monoïdale $mathcal{V}$: c'est la {em la construction des diagonaux}. Donc, pour $(mathcal{V},otimes,I)=([0,infty]^{sf op},+,0)$, les $mathcal{V}$-catégories sont les espaces métriques; et pour $mathcal{W}=mathcal{D}(mathcal{V})$ (la bicatégorie des diagonaux dans $mathcal{V}$), les $mathcal{W}$-catégories sont les espaces métriques partiels. Mais bien sûr tout espace metrique ordinaire est un espace métrique partiel; et il est aussi vrai que tout espace métrique partiel détermine (au moins) un espace métrique ordinaire. Cette relation est entièrement expliquée par des {em changements de base}, c'est à dire des foncteurs particuliers, qui existent entre $mathcal{V}$ et $mathcal{W}$. Comme autre exemple de changement de base, je vais parler de l'ordre sous-jacent d'un espace métrique, et de l'espace métrique libre sur un ordre. Je vais par ailleurs indiquer comment, par le biais des changements de base, on peut formuler des questions pertinentes à propos de ces structures. Dans mon exposé, je vais éviter toute technicité (le seul prérequis étant la notion d'ensemble ordonné), car je veux surtout insister sur l'usage de bicatégories comme base d'enrichissement pour traiter spécifiquement les phénomènes décrits ci-dessus.

Jeudi 27 février 2014 à 10h Michele Basaldella (Université d'Aix-Marseille),
Infinitary classical logic: recursive equations and interactive semantics

Résumé : (Masquer les résumés)
In this talk, we present an interactive semantics for derivations (i.e., formal proofs) in an infinitary extension of classical logic. The formulas of our language are possibly infinitary (i.e., not necessarily well-founded, and not necessarily finitely branching) trees labeled by logical connectives and propositional variables. We show that in our setting every recursive formula equation has a unique solution. As for derivations, we use an infinitary variant of the standard Tait-calculus to derive sequents. In our sequent calculus, derivations are defined to be possibly infinitary trees labeled by sequents and rules. The interactive semantics we introduce is somehow similar to Girard's ludics, inasmuch as it builds upon a suitable procedure of cut-elimination. We show a completeness theorem for derivations, that we call interactive completeness theorem.

Jeudi 20 février 2014 à 10h Luigi Santocanale (Laboratoire d'Informatique Fondamentale, Aix-Marseille Université),
Catégories mu-bicomplètes, jeux de parité, et élimination des coupures pour les preuves circulaires

Résumé : (Masquer les résumés)
Dans cet exposé je présenterai la notion de catégorie mu-bicomplète, et instancierai cette notion avec la catégorie des ensembles, via la notion de jeu de parité. J'expliquerai ensuite l'importance de chercher un syntaxe adéquate pour dénoter toutes les flèches d'une catégorie mu-bicomplète libre. Je proposerai donc la notion de preuve circulaire (avec la condition sur les cycles qu'elle doit satisfaire) comme une telle syntaxe ; je justifierai cette proposition par les résultats de correction et complétude (fortes, catégoriels) du calcul, par rapport à la sémantique catégorielle envisagée. Nous montrerons qu'un théorème d’élimination des coupures vaut, car on peut éliminer les coupures d'un preuve circulaire finie avec cut, pour obtenir un arbre de preuve infini sans cut. Nous montrerons comment ce processus d’élimination des coupures amène à caractériser toutes les fonctions d'ensembles qui sont l'image d'une flèche d'une catégorie mu-bicomplete libre.

Jeudi 06 février 2014 à 10h Laurent Vuillon (LAMA),
De la géométrie discrète à la biologie des interactions protéine-protéine

Résumé : (Masquer les résumés)
Nous montrerons dans ce séminaire comment des outils mathématiques de géométrie discrète et de théorie des pavages peuvent servir à résoudre des problèmes de bio-mathématiques et en particulier de comprendre les interactions protéines-protéines. On va ainsi montrer comment ces interactions mènent à des polymères ``normaux'', à des virus ou à des fibres...

Le séminaire de l’équipe LIMD est sous la responsabilité de Xavier Provencal.
Options : Voir par date croissante . Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2015, toutes ensemble.