J'exposerai mes idées pour une nouvelle sorte de théorème prouveur, basé sur les idées suivantes: - on crée le langage de programmation avec un système de typage statique fort le plus fort possible - on étend ce langage pour en faire une logique (on n'ajoute pas la logique au dessus du langage) Le but de ce séminaire sera de démarrer un éventuel groupe de travail ...
Je presente dans mon exposé le système de type avec intersection de J. Wells qui permet de trouver le type principal d'un lambda-terme uniquement avec l'opération "substitution". Pour cela, il ajoute d'autres variables de type dites "variables d'expansion" et definit la substitution sur ces variables. Je vous présente ensuite une sémantique de réalisabilité pour ce système et un théorème de complétude pour un de ses sous systemes. Ce travail a été fait en collaboration avec F. Kamareddine et J. Wells.
Parmi les modèles de la concurrence et de la mobilité qui ont foisonné après la définition par Milner du Pi-Calcul, on rencontre deux familles très différentes: les modèles de la communication, qui prolongent directement le Pi-Calcul , et des modèles basés sur une notion spatiale de lieux ou de places, dont un exemple bien connu est les Ambients de Cardelli et Gordon. Les Bigraphes, proposés récemment par Milner, sont une tentative d'englober ces deux courants dans une structure unique. Nous proposons une introduction aux Bigraphes, basée sur le tutoriel que Milner a présenté à Paris en septembre dernier.
Le lambda-calcul a deux modèles d'implantation principaux: les machines abstraites, utilisées pour l'appel par nom, par valeur, etc., et les réseaux d'interaction, utilisés pour la réduction optimale, les évaluateurs à la Mackie, etc. La nature très distribuée des réseaux d'interaction ne permet pas, en général, de décrire précisément la stratégie qu'ils implantent et ces deux modèles d'implantation semblent complètement déconnectés. J'établis une connexion entre ces deux mondes en proposant des traductions des stratégies habituelles du lambda-calcul dans les réseaux d'interaction. Ces traductions reposent sur l'idée très simple d'introduire un jeton d'évaluation qui séquentialise certaines réductions. Les stratégies traitées sont l'appel par nom, par valeur, par nécessité et la stratégie "fully lazy".
Nous aborderons diverses méthodes de combinatoire des mots appliquées aux mots de Sturm. En particulier, nous démontrerons des théorèmes de base de la combinatoire des mots comme le lien entre complexité et périodicité, l'équivalence entre plusieurs définitions des mots de Sturm et enfin des résultats sur les graphes des mots (graphes de De Bruijn ou de Rauzy) et la dynamique de ces graphes pour les mots de Sturm.
TBA. Slogan: comment utiliser la machine de Krivine pour linéariser les lambda-termes et rapport avec la propriété d'uniformité du lambda-calcul diff.
On définit une sémantique de réalisabilité inspirée des candidats de réductibilité de J.Y. Girard et adaptée par M. Parigot pour le cas classique. On prouve un lemme de correction pour cette sémantique. On montre ensuite la complétude pour une classe de type notée D^+. Cette classe est formée des types qui ne contiennent pas de quantificateurs à droite d'une flèche (i.e. les quantificateurs ne sont qu' à gauche des flèches). Elle contient donc, en particulier, les types de données. C'est une sous classe des types forall positifs pour lesquels la complétude n'est pas vraie (on fournit un contre exemple).
Nous montrons comment le dédoublement de la règle d'axiome du calcul des séquents de Gentzen permet de mettre en évidence un noyau de calcul qui exprime de manière syntaxique la dualité entre les notions standard d'appel par nom et d'appel par valeur. D'un point de vue théorie de la démonstration, on en conclut que l'appel par valeur est intrinséquement partie prenante de l'interprétation calculatoire du calcul des séquents. D'un point de vue théorie du calcul, on débouche sur un nouveau formalisme basé sur une profonde symétrie entre termes et contextes d'évaluation.
Les codes identifiants ont été introduits pour modéliser un problème de détection de défaillances dans des réseaux multiprocesseurs [1]. C'est un sujet récent de théorie des graphes, qui, dans une de ses variantes, se définit comme suit : étant donné un graphe G=(V,E), un code t-identifiant de G est un sous-ensemble de sommets C de V tel que tout sous- ensemble d'au plus t sommets de G soit identifié de façon unique par la trace de C sur son voisinage fermé. Formellement, C est un code t-identifiant de G si et seulement si on a N[X]cap C neq N[Y]cap C pour toute paire (X, Y) de sous-ensembles distincts d'au plus t sommets de G, où N[X] désigne l'union de X et des voisins de X dans G. Ce sujet peut être vu comme un cas particulier de problème de couverture par tests sur un ensemble structuré. Les problèmes de couverture par tests sont une large classe de problèmes combinatoires, englobant le fameux problème des fausses pièces ou les jeux populaires de devinettes. Lorsqu'un tel code existe, le problème d'optimisation discrète sous-jacent consiste à déterminer un code t-identifiant de cardi- nalité minimum. Au niveau algorithmique, ce problème est NP- difficile [2] . Dans [1], des bornes générales sont données. On peut s'intéresser à l'aspect extrémal de ce problème, en particulier on peut étudier le problème suivant : étant donné un entier n, quels sont les graphes admettant un code t-identifiant de cardinalité minimum parmi les graphes à n sommets ? Dans cet exposé je vais présenter différentes approches pour aborder cette question de combinatoire extrémale. J'exposerai tout d'abord une approche probabiliste, utilisant la notion de graphe aléatoire, qui nous permet d'obtenir une borne supérieure proche de la borne inférieure générale de [1]. Ensuite, j'expose- rai les liens étroits que l'on peut établir entre les codes identifiants et d'autres types de codes, en particulier les codes superimposés, ce qui nous permettra d'obtenir une borne inférieure améliorant celle de [1]. Enfin, je présenterai des constructions basées sur des plans projectifs. Références : [1] M. G. Karpovsky, K. Chakrabarty, L. B. Levitin, On a New Class of Codes for Identifying Vertices in Graphs, IEEE Transactions on Information Theory 44(2), 599-611 (1998). [2] I. Charon, O. Hudry, A. Lobstein, Minimizing the size of an identifying or locating-dominating code in a graph is NP-hard, Theoretical Computer Science 290(3), 2109-2120 (2003).
Les automates cellulaires sont des systèmes dynamiques discrets composés de cellules agencées régulièrement et qui interagissent localement. Bien que les interactions locales soient très simples à décrire, le comportement du système dans son ensemble est très difficile à prévoir. Dans cet exposé, je présenterai d'une part une approche formelle, basée sur des pré-ordres de simulation, pour comparer et classifier les dynamiques globales de ces objets. Je montrerai comment des classes d'automates définies par des propriétés dynamiques classiques se traduisent dans la structure de ces pré-ordres. Je présenterai également une construction qui permet d'obtenir divers ordres-induits remarquables de certains pré-ordres de simulation, ainsi qu'un automate cellulaire intriguant, capable de simuler le comportement d'une machine de Turing avec un nombre fini arbitrairement grand de têtes de calcul, mais qui interdit la cohabitation simultannée d'un nombre infini de têtes. J'aborderai d'autre part les automates cellulaires comme des objets syntaxiques et étudierai la densité de diverses propriétés de ces objets. Je montrerai comment une contrainte syntaxique locale permet de définir une classe (les automates cellulaires captifs) dans laquelle les propriétés monotones suivent une loi zéro-un. En particulier je montrerai que, dans cette classe, la propriété d'être intrinsèquement universel a une densité 1 tout en étant indécidable.
La logique quantique, qui est une composante importante des travaux visant à la compréhension du monde quantique, reste mal comprise et difficilement utilisable en pratique. Grâce à la mise en évidence de l'importance de notions "classiques" comme les points de vue ou la connaissance partielle, nous montrons comment il est possible d'obtenir de nouvelles pistes pour l'étude de ce type de logique, avec en particulier des méthodes de recherche automatique de preuves. Dans cet exposé, nous présenterons un ensemble de résultats nous effectuerons une présentation de la logique quantique ainsi que le modèle usuel de cette logique, à savoir les treillis orthomodulaires. Ensuite, nous exposerons une approche utilisant les "systèmes de représentation" (développés par l'auteur durant sa thèse de doctorat, voir bibliographie) basée sur les notions de connaissance partielle et de points de vue qui permet de fournir une caractérisation purement classique et non probabiliste (basée sur l'utilisation d'algèbres booléennes). Nous montrerons enfin comment cette caractérisation permet d'envisager la logique quantique d'une nouvelle manière, et fournir de nouveaux outils pour son étude. En particulier, nous présenterons un fragment décidable de cette logique, sous forme de calcul des séquents. Références: http://www-leibniz.imag.fr/~obrunet
Dans cet exposé nous présenterons deux formalismes de réécriture d'ordre supérieur permettant l'utilisation de filtrage "à la ML". Le premier de ces formalismes, le lambda P calcul, est une extension du calcul lambda sigma traitant de manière complètement explicite les notions de substitution et de filtrage. Nous montrerons qu'il possède les propriétés de normalisation forte sur les termes typés et de confluence. Le second formalisme est un formalisme de réécriture d'ordre supérieur fondé sur les (S)ERS. Ce formalisme autorise la définition de systèmes de réécriture utilisant la notion de filtrage. Nous donnerons un critère syntaxique de confluence pour de tels systèmes.
On considère un polyèdre, on définit alors le billard polyédral de la facon suivante: On part d'un point d'une face, on se donne une direction et on se déplace dans cette direction jusqu'à rencontrer une autre face. On obtient un nouveau point, la direction est alors réfléchie orthogonalement par rapport à cette face. Pour étudier cette application on repère chaque face par une lettre, l'orbite d'un point devient une suite de lettres. C'est ce qu'on appelle un mot. Le but est d'étudier ces mots grace en autre à leurs fonctions de complexité. Nous présenterons les estimations connues pour un polyèdre général, et nous nous intéresserons plus précisemment au cas du cube.
Dans cet exposé, on développera une interprétation de la logique linéaire en termes de processus concurrents. On utilise pour cela une variante du pi-calcul, munie d'une notion paramétrable d'observation (divergence, may- ou must-testing...), d'où l'on déduit une notion abstraite de comportement. La structure de ces comportements mène à la définition de connecteurs logiques, inspirés des logiques spatiales et temporelles, qui décrivent les propriétés fondamentales des processus. Le système obtenu est une forme de logique linéaire qui définit pour le pi-calcul un système de type qui garantit de bonnes propriétés comme la terminaison et l'absence de blocage. D'autre part, ce système de type établit une correspondance à la Curry-Howard entre la concurrence et diverses variantes de logique linéaire, qui s'intègre bien aux précédentes études sur la décomposition du calcul fonctionnel dans les calculs concurrents.
Dans cet exposé, je présenterai la structure de polygraphe, une sorte de complexe cellulaire, à travers ses liens avec la réécriture et la logique. Dans la première partie, nous verrons comment tout système de réécriture de termes peut être traduit sous la forme d'un polygraphe, vu ici comme un système de réécriture de circuits. Sur un exemple, je montrerai comment construire des ordres de terminaison adaptés à ces objets. Dans la seconde partie, nous traduirons le calcul propositionnel et ses démonstrations en un polygraphe : cela permet d'obtenir des représentations bidimensionnelles pour les formules et tridimensionnelles pour les démonstrations. Enfin, si le temps le permet, je parlerai d'une piste menant à une autre description polygraphique des démonstrations classiques, toujours en trois dimensions.
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é.