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

Year 2005

Thursday 8th December 2005 at 10h15 Patrick Thévenon
Typage avec deux flèches

Abstract: (Hide abstracts)
Dans le cadre des grammaires catégorielles abstraites (ACG) introduites par Ph. de Groote, on peut faire des traductions entre différentes structures linguistiques, par exemple syntaxiques et sémantiques. Initialement conçu sur la base du lambda-calcul linéaire utilisé en linguistique, l'expressivité se trouve limitée notamment en sémantique, où l'on souhaiterait utiliser plusieurs fois une même variable. L'idée est alors d'introduire de l'intuitionisme, et donc un lambda-calcul avec deux types de variables et deux types de flèches (intuitionnistes et linéaires). Il est alors naturel de se demander quel peut être le type principal de termes de ce calcul, et quelles sont ses propriétés. Une difficulté provient du fait que lors de la recherche du type principal, des flèches sous-spécifiées peuvent apparaître, qui peuvent indifféremment être remplacées par les flèches linéaires ou des flèches intuitionistes. Pour ne pas compliquer ce lambda-calcul, il serait agréable de trouver des fragments pour lesquels on pourrait donner une notion de type principal sans flèche sous-spécifiée. Dans le cas général nous verrons que c'est impossible, mais que pour deux cas, le cas eta-long et le cas linéaire, nous avons un résultat.

Thursday 8th December 2005 at 10h Stephane Le Roux (ENS Lyon),
Théorie des jeux sans probabilité

Abstract: (Hide abstracts)
Les jeux simultanés sont des objets représentant le scénario informel suivant : des agents effectuent simultanément chacun un choix parmi un ensemble (propre à chaque agent) de choix possibles. En fonction des tous ces choix, on attribue alors un gain à chaque agent. Et c'est tout, le jeux est terminé. Nash a défini une notion d'équilibre dans ces jeux mais il existe des jeux sans équilibre. Si les agents et les choix sont en nombre fini, Nash a montré qu'on pouvait construire d'un jeu une version "probabilisée" qui, elle, possède un équilibre. J'espère montrer lors de ce groupe de travail que l'introduction des probabilités n'était pas la seule solution envisageable. Deux directions possibles sont : 1) Introduire le non déterminisme sans proba. 2) Considérer la structure "la plus générale" dans laquelle on peut définir les équilibres à la Nash et insister sur l'aspect dynamique qui mène à la notion d'équilibre. Dans les deux cas, les concepts sont plus simples que les proba et les équilibres sont calculables. De plus, les ensembles d'équilibres possèdent des propriétés algébriques alors que les équilibres probabilistes sont peu structurés.

Monday 5th December 2005 at 14h Jakub Kozik (Jagiellonian University),
Decidability of density problem for languages

Abstract: (Hide abstracts)
Notion of density is used when there is a need of quantitative considerations on countable sets. It is known fact that it is impossible to construct uniformly distributed probabilistic measure on such set. By now, standard approach to deal with this problem is to consider asymptotic behavior of probabilities in finite subsets of elements of bounded size. The well known results of such approach are 0-1 laws in logic. In the theory of formal languages notion of density was introduced by Berstel. First approaches were focused on regular languages and exploited the theory of formal power series. Natural extension is the notion of conditional density. For any language L let l_n denote number of words of length n in L. Let L,S be languages over finite alphabet such that S is a subset of L. Let p_n denote probability that randomly and uniformly chosen word from L of length not greater than n belongs to S. Language S has conditional density in L if and only if there exists the limit of p_n. Many problems, concerning asymptotic properties of predicate logic formulae with bounded number of variables, can be rephrased in the theory of languages using the above definition. For the classes of grammars C,D the problem of having conditional density is defined as follows: Given two grammats G_L belonging to C and G_S belonging to D, decide whether L(G_S) has conditional density in L(G_L). In my talk I am going to present my result concerning decidability of the problem of conditional density for several classes of grammars.

Thursday 1st December 2005 at 10h15 Christophe Raffalli
Typage sans types, preuve de la préservation du type.

Abstract: (Hide abstracts)
Je donnerai les définitions de bases et la preuve de subject-reduction de mon système.

Thursday 1st December 2005 at 10h Radu Mateescu (INRIA),
Communication mobile à travers des portes immobiles

Abstract: (Hide abstracts)
Les calculs de processus mobiles, tels que le pi-calcul, sont bien adaptés à la description des systèmes distribués comportant des canaux de communication mobiles et des processus qui sont créés/détruits dynamiquement. En revanche, les algèbres de processus classiques, telles que CCS, CSP ou ACP, ne permettent pas une description directe de la mobilité, mais bénéficient d'environnements de simulation et de vérification plus développés. Dans cet exposé, je présenterai une traduction d'un fragment du pi-calcul vers LOTOS et E-LOTOS (des normes ISO issues de CCS et CSP), qui permet de simuler la communication sur des canaux mobiles. Je préciserai également quelques pistes de recherche pour étendre cette traduction vers des fragments plus larges du pi-calcul.

Thursday 24th November 2005 at 10h Claudia Faggian et Patrick Baillot
Meta interactions

Abstract: (Hide abstracts)
Séance informelle sur la ludique ou la complexité implicite ou les relations entre ludique et calculs de processus.

Thursday 17th November 2005 at 10h15 Anne Bouillard (LIP ENS Lyon),
Etude combinatoire et asymptotique du groupe de traces

Abstract: (Hide abstracts)
Un groupe de traces est le quotient d'un groupe libre par des relations de commutation entre certaines lettres. On peut représenter les traces par des tas de pièces colorées. Dans une première partie, nous étudions les groupes de traces d'un point de vue combinatoire et obtenons une formule explicite de la série génératrice d'un groupe de traces, comparable à la formule d'inversion de Möbius pour le monoïde de traces. Dans un deuxième temps, nous utilisons cette formule pour étudier le taux de croissance moyen asymptotique d'un tas de pièces colorées.

Thursday 3rd November 2005 at 10h Christophe Raffalli (LAMA (université de Savoie)),
Typing without types (Types as programs)

Abstract: (Hide abstracts)
We present a new approach to the problem of static typing in languages of the ML family. The basic idea is to generalize the pseudo linear unification algorithm you can use in the Hindley-Milner algorithm. The obtained language is very expressive compared to existing ML implementation and do not require type annotation for many features of ML that usually needs some (like modules, object, ...).

Thursday 13th October 2005 at 14h15 Fairouz Kamareddine (Heriot-Watt University, Edinburgh, Scotland),
Théorie des types

Abstract: (Hide abstracts)
La théorie de types a été inventée au début du 20eme siècle avec le but d'éliminer les paradoxes qui viennent de l'application d'une fonction à elle-même. Le lambda calcul a été développé (par Church) vers 1930 comme une théorie de fonctions. En 1940, Church ajoutait les types à son lambda calcul. Ces types étaient simples, ce qui veut dire qu'ils n'étaient jamais construits par des lieurs (comme un $lambda$). Alors, on a des termes comme $lambda_{x:T}.B$ (qui sont construits par le lieur $lambda$) mais on n'a pas des lieurs qu'on peut utiliser pour construire un type. Malgré l'influence qu'a connue le lambda calcul typé de Church, sa limitation a aboutit a la création de plusieures théories de types dans la deuxième partie du 20eme siècle. Dans ces calculs, les types sont construits par des lieurs. Dans la plupart de ces calculs, on trouve deux lieurs : le $lambda$ (pour construire des termes) et le $Pi$ (ou $forall$, pour construire des types). Ces deux lieurs nous permettent de distinguer les fonctions (qu'on construit avec les $lambda$s) des types (qu'on construit avec les $Pi$). En plus, dans ces calculs, on permet bien la $beta$-réduction mais pas la $Pi$-réduction. Autrement dit, dans ces calculs on a bien la règle : $(lambda_{x:A}.B)C rightarrow B[x:=C]$ Mais pas la règle : $(Pi_{x:A}.B)C rightarrow B[x:=C]$ En particulier, lorsque $b$ a le type $B$, on donne à $(lambda_{x:A}.b)C$ le type $B[x:=C]$ à la place de $(Pi_{x:A}.B)C$. Il y a quelques extensions puissantes des théorie des types qui donnent le même comportement au $Pi$ qu'au $lambda$ (par exemple, en Automath, dans le langage de programmation Henk de Simon Peyton Jones, etc.). Ca nous aboutit à poser la question : pourquoi distinguer entre le $lambda$ et le $Pi$ lorsque des systèmes comme Automath nous montrent qu'il est plus avantageux de traiter les types exactement comme les termes? Dans cette présentation je décrit un système ou les deux lieurs sont identifiés et je montre que ce système a toutes les propriétés qu'on désire d'un système de typage sauf pour l'unicité des types. Mais je démontre aussi que cette perte de l'unicité des types n'est pas grave parce qu'il y a un isomorphisme entre le typage avec deux lieurs et le typage avec un seul lieur et en plus, tous les différent types d'un même terme, suivent le même modèle.

Thursday 22nd September 2005 at 10h Rene Vestergaard (JAIST (Japon)),
Reasoning about Languages with Binding: a first-order foundation and full adequacy

Abstract: (Hide abstracts)
We will look at what is involved in formally proving results about languages with binding. We will in particular focus on what we want to prove, what we actually do prove, and what requirements we need to put on the formalisms that we use.

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