Les travaux présentés dans cet exposé se situeront au carrefour de la géométrie discrète et de la combinatoire des mots. Je m'intéresserai en particulier aux relations entre ces disciplines et montrerai, comment obtenir de nombreuses propriétés (propriétés structurelles, statistiques...) des plans et surfaces discrets (analogues discrets des plans et des surfaces usuels) à partir d'un codage des ces objets par des mots bidimensionnels indexés par Z2. Je terminerai mon exposé par l'énoncé de quelques perspectives de recherches ainsi que quelques questions ouvertes auxquelles je m'intéresse actuellement.
En partant d'une structure généralisant les graphes de transitions et les simulations, je montrerai comment relier les notions de programmes (ceux de la vraie vie) et de fonctions continues (celles de la topologie constructive). Ceci donne un contenu concret à la 171 topologie formelle 187 de Giovanni Sambin et peut-être vu comme une extension de l'isomorphisme de Curry-Howard. De plus tous les résultats peuvent être développés dans la théorie des types dépendants 171 à la suédoise 187. Plus généralement, la notion utilisée permet de décrire tout phénomène interactif entre un utilisateur et son environnement. La structure résultante permet, entre autre, de donner un modèle non-trivial du lambda-calcul différentiel et semble ainsi relier deux visions des calculs de processus. (??)
We prove the correctness of an original method for generating components that capture the occurrence of events, and monitor logical and temporal properties of hardware/software embedded systems. The properties are written in PSL, under the form of assertions in declarative form. The method is based on a library of primitive digital components for the PSL temporal operators. These building blocks are interconnected to construct complex properties, resulting in a synthesizable digital module that can be properly linked to the digital system under scrutiny.
Le lambda mu calcul symétrique (i.e. le calcul où on a ajouté la règle mu' duale de mu) est fortement normalisable dans le cas typé. Pourtant quand on ajoute la règle rho qui semble n'être qu'une règle de simplification, la forte normalisation est perdue. On garde cependant la faible normalisation. C'est ce qu'on montrera dans cet exposé.
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.
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.
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.
Je donnerai les définitions de bases et la preuve de subject-reduction de mon système.
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.
Séance informelle sur la ludique ou la complexité implicite ou les relations entre ludique et calculs de processus.
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.
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, ...).
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.
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.