The seminar of the team LIMD is under the responsibility of Sebastien Tavenas.
Settings: See with increasing date . Hide abstracts
Other years: 2005, 2006, 2007, 2008, 2009, 2010, 2012, 2013, 2014, 2015, 2016, 2017, all years together.

Year 2011

Thursday 15th December 2011 at 10h Annette Casagrande (LAMA, LIMD),
Proposition d'une mesure de voisinage entre textes Application à la veille stratégique

Abstract: (Hide abstracts)
Nous proposons une méthode de calcul de proximité entre textes, appelée mesure de voisinage. Cette mesure est basée sur la présence de mots communs, de synonymes et de mots cooccurrents. Nous comparons cette mesure à la similarité cosinus, utilisée en Recherche d'Informations, au travers de trois bases de données différentes. Nous avons développé un prototype, nommé ALHENA, utilisé dans le domaine de la veille stratégique anticipative (VAS). L'expérimentation menée sur la valorisation du CO2 a montré l'utilité du prototype dans le processus de VAS, face au problème de la surcharge d'information notamment occasionnée par l'usage de l'Internet.

Thursday 1st December 2011 at 10h Karim Nour (LAMA, LIMD),
About the range property for H

Abstract: (Hide abstracts)
Recently, A. Polonsky has shown that the range property fails for H. We give here some conditions on a term F that imply that its range has cardinality either 1 or infinity. L'exposé sera accessible à tous les membres de l'équipe.

Thursday 17th November 2011 at 10h Krzysztof Worytkiewicz (LAMA),
Simulations as homotopies

Abstract: (Hide abstracts)
We exhibit a model structure on 2-Cat. A certain class of homotopies in this model structure turns out to be in 1-to-1 correspondence with strong simulations among labeled transitions systems, formalising the geometric intuition of simulations as deformations. The correspondence still holds in the cubical setting, characterising simulations of higher-dimensional transition systems (HDTS).

Thursday 20th October 2011 at 10h Lionel Vaux (LDP, IML),
On the transport of finiteness structures

Abstract: (Hide abstracts)
Finiteness spaces were introduced by Ehrhard as a model of linear logic, which relied on a finitess property of the standard relational interpretation and allowed to reformulate Girard's quantitative semantics in a simple, linear algebraic setting. I will review recent results obtained in a joint work with Christine Tasson, providing a very simple and generic construction of finiteness spaces: basically, one can ``transport'' a finiteness structure along any relation mapping finite sets to finite sets. Moreover, this construction is functorial under mild hypotheses, satisfied by the interpretations of all the positive connectives of linear logic. Recalling that the definition of finiteness spaces follows a standard orthogonality technique, fitting in the categorical framework established by Hyland and Schalk, I will show that the features of transport do not stand on the same level as the orthogonality category construction; rather, they provide a simpler and more direct characterization of the obtained structure, in a webbed setting. PS: Although I have slides (in english) ready for this presentation, it is best enjoyed in its chalk and blackboard version so I will stick to the latter.

Thursday 6th October 2011 at 10h Tim Porter (WIMCS, University of Bangor),
Homotopical Aspects on Multiagent Systems

Abstract: (Hide abstracts)
The epistemic logic used for n-agent systems is the modal logic $S5_n$. In this talk I will briefly look at the Kripke semantics of this, how it relates to simple models of multiagent systems, and then will explore some ideas that make some tentative steps in the direction of modelling the flow information and knowledge in such systems. (The last part will raise more problems and questions than it answers but that is the fun of it!!! Since the paper below was written, directed homotopy has been developed more and it remains to be seen if it can be used to describe evolving multi-agent systems. I will discuss this beyond the prepared slides, if there is time.) (As I have slides in English, I will give the talk in that language.) Ref: Interpreted systems and Kripke models for multiagent systems from a categorical perspective, Theoretical Computer Science, 323 (2004) pp. 235-266.

Thursday 29th September 2011 at 10h Pawel Gladki (AGH University of Science and Technology, Kraków, Poland),
Quotients of index two of the space of orderings of the field Q(x)

Abstract: (Hide abstracts)
Let $(X,G)$ be a space of orderings, let $G_0$ be a subgroup of index $2$ in $G$, $-1 in G_0$, and let $X_0$ denote the set of restrictions $X restriction G_0$ of elements of $X$ (viewed as characters on $G$) to characters on $G_0$. We search for necessary and sufficient conditions on $G_0$ for $(X_0,G_0)$ to be a quotient of $(X,G)$. In particular, we discuss the case when $(X,G)$ is the space of orderings of the field $Q(x)$. The talk is intended for a broad audience and all definitions necessary to follow the exposition will be explained in details. This is joint work with Murray Marshall.

Thursday 22nd September 2011 at 10h Pierre Hyvernat (LIMD),
Foncteurs polynomiaux, jeux et logique linéaire (différentielle)

Abstract: (Hide abstracts)
Les « systèmes d'interaction » étaient à l'origine un moyen de représenter une notion de « jeux » en théorie des types. On obtient de cette manière une catégorie de jeux et de simulations qui modélise la logique linéaire différentielle. De manière assez surprenante, la dynamique ne joue aucun rôle dans la définition de composition des stratégies ! Cette notion de jeux existe sous des noms différents : « containers » (Ghani, Altenkirch, Hancock, ...) ou « foncteurs polynomiaux » (Hyland, Kock, Gambino, ...). Ce qui change ici est la notion de morphisme, plus générale que dans la littérature existante. Après une petite introduction, je montrerais les liens entre ces polynômes (point de vue intentionnel) et les foncteurs associés (point de vue extensionnel). Je construirais ensuite le modèle de (D)ILL en insistant sur l'interprétation en termes de jeux et les similarités formelles avec le modèle « dégénéré » des transformateurs de prédicats. Je ne ferais probablement aucune preuve, mais je mentionnerais quand même l'outil important, à savoir le langage interne des catégories localement cartésiennes fermées (càd la théorie des types dépendants)...

Thursday 7th July 2011 at 10h09 Pierre Hyvernat (LIMD),
Petit casse-tête combinatoire : sections non-ordonnées et fonctions booléennes strictement croissantes

Abstract: (Hide abstracts)
On muni les tuples d'ensembles d'entiers (X1, ..., Xn) de l'ordre suivant : (X1, ..., Xn) < (Y1, ..., Yn) si les Xs ont plus de « sections non-ordonnées » que les Ys. L'équivalence engendré par ce préordre est très simple, mais la preuve, bien qu'élémentaire, l'est moins (il s'agit d'un petit casse-tête amusant...). Je caractériserais cette équivalence (avec la preuve) ainsi que les liens entre cet ordre et l'inclusion toute simple. La preuve utilise la notion de fonction booléenne strictement croissante, qui semble ne pas apparaitre souvent dans la littérature. Je montrerais quelques unes de leurs propriétés. Pré-requis : notion d'ordre, de permutation, de quotient. (niveau L1)

Thursday 30th June 2011 at 11h Yukiko Kenmochi (Laboratoire d'Informatique Gaspard-Monge, Université Paris-Est),
L'ajustement robuste d'un hyperplan discret

Abstract: (Hide abstracts)
Nous considérons le problème d'ajustement suivant : étant donné un ensemble de N points dans une image numérique en dimension d (i.e. Z^d), trouver un hyperplan discret qui contient le plus grand nombre possible de points. En utilisant un modèle discret pour l'hyperplan, nous montrerons que nous pouvons générer tous les ensembles de consensus possibles pour ajuster le modèle, et présenterons une méthode exacte pour d=2,3 dont la complexité en temps est O(N^d log N) et celle en espace est O(N). Ces complexités ont naturellement motivé l'amélioration. Nous avons ensuite observé que le problème est 3SUM-difficile pour d=2 de sorte qu'il ne peut probablement pas être résolu exactement avec une complexité meilleure que O(N^2), et il est conjecturé que la complexité optimale en dimension d est en fait O(N^d). Nous proposons donc deux méthodes approximatives de complexité linéaire en temps.

Thursday 16th June 2011 at 14h30 Mohamad Ziadeh (LIMD),
Completness for simply typed lambda mu calculus

Abstract: (Hide abstracts)
Between the important thing, when we deal with a type or a formula A of a system of typing that satisfies the strong normalization S.N., is to build a set of terms that satisfies 'a term in the set corresponding to A is equivalent to say that t is of type A. Unfortunally it is impossible to have this equivalency because of S.N., so the work take another formulation to escape this problem and it becomes 'a term in the set corresponding to A is equivalent to say that t is in relation with t' which is of type A'. many studies having this form where been published for many systems and relations. My work will be around the simply typed system in lambda mu calculus.

Thursday 9th June 2011 at 10h Nicolas Michel (EPFL),
TBA

Abstract: (Hide abstracts)
La définition des différentes K-théories suit le schéma suivant. Etant donné un objet C, on lui associe d'abord une catégorie AC qui est « structurée » (symétrique monoïdale, exacte, Waldhausen, …). On applique ensuite une « machine » de K-théorie sur AC pour obtenir finalement le spectre de K-théorie de l'objet C. Par exemple, on associe à un anneau R sa catégorie de modules projectifs de type fini pour obtenir la K-théorie usuelle de R. Dans ma thèse, je me suis intéressé à la première étape de ce processus. Plus précisément, je me suis posé les questions suivantes. Quels types d'objets admettent une notion intéressante de K-théorie ? Quelles catégories structurées devrait-on associer à ces objets pour obtenir une information K-théorique à leur sujet ? Finalement, comment cette correspondance prend-elle en compte les morphismes de ces objets ? Je vais décrire un cadre conceptuel qui permet de traiter de manière unifiée de nombreux exemples et qui apporte de nouveaux outils pour les étudier. Je prendrai l’exemple de la K-théorie des schémas comme fil conducteur.

Thursday 26th May 2011 at 10h03 Christophe Raffalli (LIMD),
(Co-)Inductive type : subtyping may be enough

Abstract: (Hide abstracts)
We present here a strongly normalizable extension of second order functional arithmetics (AF2) with subtyping, that allows to program with recursive types in the pure lambda-calculus (i.e., without constant). It assigns types to the Scott encoding of algebraic datatypes and to the recursor on those types. Thus, it answers the open question of finding a strongly normalizing type system which allows to program on Scott numerals. One of the key features of the system is to have no more typing rules than AF2. The new rules are only subtyping rules. The first-order layer is used to prove the correction of extracted programs. It is also worth noticing that in this system union type (both finite and infinite) are definable and still the system enjoys subject-reduction.

Thursday 19th May 2011 at 10h05 Luidnel Maignan (INRIA Saclay),
Points, Distances and Cellular Automata: Geometric and Spatial Algorithmics

Abstract: (Hide abstracts)
Spatial computing aims at providing a scalable framework where computation is distributed on a uniform computing medium and communication happen locally between nearest neighbors. We study the particular framework of cellular automata, using a regular grid and synchronous update. As a first step towards generic computation, we propose to develop primitives allowing to structure the medium around a set of particles. We consider three problems of geometrical nature: moving the particles on the grid in order to uniformize the density, constructing their convex hull, constructing a connected proximity graph establishing connection between nearest particles. The last two problems are considered for multidimensional grid while uniformization is solved specifically for the one dimensional grid. The work approach is to consider the metric space underlying the cellular automata topology and construct generic mathematical object based solely on this metric. As a result, the algorithms derived from the properties of those objects, generalize over arbitrary regular grid. We implemented the usual ones, including hexagonal, 4 neighbors, and 8 neighbors square grid. All the solutions are based on the same basic component: the distance field, which associates to each site of the space its distance to the nearest particle. While the distance values are not bounded, it is shown that the difference between the values of neighboring sites is bounded, enabling encoding of the gradient into a finite state field. Our algorithms are expressed in terms of movements according to such gradient, and also detecting patterns in the gradient, and can thus be encoded in finite state of automata, using only a dozen of state.

Tuesday 17th May 2011 at 10h06 Vincenzo Ciancia (Amsterdam, ILLC),
Labelled transition systems with interfaces and symmetry: coalgebras in a presheaf category and their finite representations

Abstract: (Hide abstracts)
In this talk, we discuss how to model in a finite way the semantics of resource-allocating interactive programs. Surprisingly, in doing so, the notion of behavioural symmetry arises from the framework, and is necessary to recover canonical models. Behavioural symmetry expresses properties relating the semantics of a program and the available resources at each state, e.g. ``the distinguished variables x and y have the same observable effect, and swapping them does not affect the semantics of the program''. Labelled transition systems (LTSs) have been successfully used to model the semantics of interactive programming languages. Their natural equivalence relation, the so-called bisimilarity, is a fundamental tool for the study of such languages. However, when resources (e.g. memory locations) can be allocated and de-allocated along transitions, bisimilarity becomes a non-standard notion (cf. the pi-calculus). The categorical abstraction of coalgebras generalises LTSs and has an associated, general definition of behavioural equivalence, coinciding with bisimilarity for LTSs. Presheaves generalise classical sets; elements of presheaves have intensional features such as interfaces, or resources, and operations on them. By using coalgebras in a category of presheaves, bisimilarity in the presence of resource allocation is recovered from the standard categorical definition. However, the obtained transition systems become infinite state machines because of fresh resources. An equivalence between categories of presheaves and of families recovers a finite representation for memory-bound programs. An associated notion of symmetry is necessary for the equivalence to hold, and for final systems (=canonical models) to exist, giving rise to behavioural symmetry.

Thursday 12th May 2011 at 10h06 Tom Hirschowitz (LAMA (LIMD)),
Introduction aux faisceaux

Abstract: (Hide abstracts)
Cet exposé, faisant suite au précédent sur les préfaisceaux, est une introduction aux faisceaux, un autre important outil catégorique dérivé des premiers. Je rappellerai le lemme de Yoneda, puis définirai les notions de crible, topologie de Grothendieck et enfin faisceau, en m'appuyant sur des exemples et contre-exemples. Si le temps le permet, je survolerai le théorème du faisceau associé, qui construit un faisceau à partir d'un préfaisceau arbitraire (si Christophe est là, on parlera de PML). Enfin, peut-être, je raconterai en deux mots mon travail avec Damien Pous, qui repose sur une description en termes de faisceaux des stratégies dites ``innocentes'' en sémantique des jeux.

Thursday 21st April 2011 at 10h Lionel Nguyen Van Thé (LATP (Marseille)),
Théorie de Ramsey, points fixes d'actions de groupes et correspondance de Kechris-Pestov-Todorcevic

Abstract: (Hide abstracts)
En 1998, Pestov montra que le groupe G des automorphismes des rationnels (vus comme ensemble ordonné) est extrêmement moyennable, c'est-à-dire que toute action continue de G sur tout espace topologique compact admet un point fixe. Pour ce faire, il démontra que la propriété énoncé ci-dessus est équivalente au théorème de Ramsey fini. Ce résultat constitue le point de départ des travaux de Kechris, Pestov et Todorcevic, qui établirent en fait qu'il s'agit là d'un phénomène général liant théorie de Ramsey pour certaines classes de structures finies (classes de Fraïssé) et moyennabilité extrême pour certains groupes topologiques. Le but de cet exposé sera de présenter la correspondance de Kechris-Pestov-Todorcevic ainsi que certaines de ces conséquences.

Thursday 14th April 2011 at 10h Tom Hirschowitz (LAMA (LIMD)),
Introduction aux prefaisceaux

Abstract: (Hide abstracts)
Cet exposé est une introduction aux préfaisceaux, un important outil catégorique. Je reprendrai du début: catégories, foncteurs, transformations naturelles, en considérant de nombreux exemples petits et gros. Je concluerai par le lemme de Yoneda en donnant l'exemple des graphes.

Thursday 31st March 2011 at 10h14 Peter G. Hancock (University of Strathclyde),
Distillation of inductive-recursive definition

Abstract: (Hide abstracts)
`IR' is a powerful principle for in the context of dependent type-theory, for defining simultaneously a set U *inductively*, with a function T : U -> D *recursively*. D may be `large', eg the type of Sets, and a paradigm example is a universe of (codes for) sets. I will try to motivate and illustrate this principle. Using containers (a particular kind of endofunctor on Set), one can distill out the essence of IR in an extremely compact, memorable form. I will try to give a tour of the distillery.

Thursday 24th March 2011 at 10h11 Alina FIRICEL (Institut Camille Jordan),
Automates finis et séries de Laurent algébriques

Abstract: (Hide abstracts)
Dans cet exposé, nous montrerons comment utiliser la combinatoire des mots et la théorie des automates afin d'étudier certaines propriétés arithmétiques des séries de Laurent à coefficients dans un corps fini. En particulier, à l'aide d'une méthode inspirée par un article d'Adamczewski et Cassaigne, nous donnerons une majoration générale de l'exposant d'irrationalité des séries algébriques. Nous illustrerons cette approche à l'aide de quelques exemples.

Thursday 17th March 2011 at 10h11 Peter G. Hancock (University of Strathclyde),
Logarithms and exponentiality

Abstract: (Hide abstracts)
I shall dust off some work by Bohm, on arithmetical features of combinatory logic. The natural combinators for addition, multiplication, exponentiation and nihilation of Church satisfy some pleasing algebraic laws resembling those of ordinal arithmetic. But they also satisfy and some other ''wild'' laws (resembling nothing arithmetical) in virtue of which they are combinatorially complete. Because of that, they support a notion of logarithm (with respect to a ''base''). I may add some remarks on ''exponentiality'', which says that two ''numbers'' are the same if they have the same behaviour as exponents.

Thursday 10th February 2011 at 10h03 Vincent Nesme (University of Potsdam),
Automates cellulaires linéaires et fractales

Abstract: (Hide abstracts)
Tout le monde aime les automates cellulaires, tout le monde aime les fractales, et l'on sait bien que celles-ci peuvent être produits par ceux-là. Par exemple, le triangle de Sierpinski, comme il s'agit du triangle Pascal modulo 2, est le diagramme espace-temps limite d'un automate cellulaire correspondant à la relation C(n+1,k+1)=C(n,k)+C(n,k+1). Plus généralement, il est connu que si l'alphabet a une structure d'anneau commutatif et que l'automate cellulaire est un morphisme d'anneaux - on parle alors d'automate cellulaire linéaire - une structure fractale va émerger de ses diagrammes espace-temps. Remplaçons maintenant l'anneau par un simple groupe - non, pas un groupe simple, un simple groupe abélien fini. J'expliquerai pourquoi, à mon sens, c'est dans ce cas plus général qu'on devrait parler d'automate cellulaire linéaire, et non pas seulement dans le cas des anneaux comme on le fait habituellement ; et surtout, je tâcherai de faire comprendre pourquoi leurs diagrammes espace-temps ont aussi des propriétés fractales.

Thursday 20th January 2011 at 10h07 Pierre Hyvernat (LIMD),
Le principe du ``size-change termination'' pour les langages avec constructeurs

Abstract: (Hide abstracts)
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).

Thursday 13th January 2011 at 10h03 Thomas Seiller (Institut mathématique de Luminy),
Graphes d'interaction

Abstract: (Hide abstracts)
Je présenterai un modèle localisé de la logique linéaire multiplicative basé sur des graphes à partir duquel il est possible d'obtenir une catégorie *-autonome ainsi que de définir une notion de vérité. Je montrerai également qu'une restriction de ce modèle à une certaine classe de graphes se plonge dans la géométrie de l'interaction hyperfinie de Girard. Ceci permet d'appréhender de manière purement combinatoire le cadre utilisant des éléments d'analyse fonctionnelle avancés introduit par Girard. J'expliquerai enfin comment adapter ce modèle pour l'étendre à la logique linéaire multiplicative-additive, et discuterai d'une extension aux exponentielles.

The seminar of the team LIMD is under the responsibility of Sebastien Tavenas.
Settings: See with increasing date . Hide abstracts
Other years: 2005, 2006, 2007, 2008, 2009, 2010, 2012, 2013, 2014, 2015, 2016, 2017, all years together.