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

Year 2006

Thursday 14th December 2006 at 11h Philippe Audebaud
Vérification formelle d'algorithmes probabilistes dans coq

Abstract: (Hide abstracts)
Cet exposé s'appuit sur le langage lambdaO (Park, Pfenning et Thrun), un langage fonctionnel typé pur étendu avec une notion de variable aléatoire. C'est un travail commun avec Christine Paulin. Après en avoir donné une présentation succinte, et illustré son pouvoir expressif, nous abordons des aspects sémantiques. Nous en proposons une sémantique dénotationnelle directe, à partir de laquelle nous produisons mécaniquement un système d'inférence pour la sémantique axiomatique à la Hoare. Des exemples de preuves en correction partielle sont proposés ; la correction totale est abordée, mais le cadre formel n'est pas complet à ce jour. Enfin, nous indiquerons comment la vérification d'algorithmes (fonctionnels) probabilistes est envisagée dans la suite de notre travail.

Thursday 7th December 2006 at 10h15 Guillaume Theyssier
Attention, une Conwayrie peut en cacher une autre.

Abstract: (Hide abstracts)
En recherchant des résultats sur la suite de Conway et le (fameux ?) théorème cosmologique, Pierre est tombé sur un article pour le moins intrigant du même monsieur. Considérez la suite (ordonnée) de fractions suivante : 17/91 78/85 19/51 23/38 29/33 77/29 95/23 77/19 1/17 11/13 13/11 15/2 1/7 55/1 Partez de l'entier 2 et à chaque étape multipliez l'entier courant par la première fraction pour laquelle le produit est entier et répétez le processus. Vous obtenez la suite des 2^p où les p sont les nombres premiers consécutifs. Un miracle pensez vous ? Non, un simple exemple de programme d'un langage de programmation universel : FRACTRAN.

Wednesday 6th December 2006 at 09h A Ranta
Grammars as Software Libraries

Abstract: (Hide abstracts)
Libraries are a major instrument of software engineering, making it possible to reuse code and to distribute labour between programmers with different areas of expertise. The sophisticated application programs we have today would not be possible without huge libraries in areas such as data structures, numerical analysis, signal processing, and computer graphics. Grammars of natural languages are a domain of a lot of expert knowledge, which it would be useful to find in software libraries. However, typical implementations of grammars are monolithic application programs, such as parsers tuned to a particular corpus. New applications typically have to build their grammars from scratch, which makes it costly to build programs such as natural-language interfaces, or to perform high-quality software localization. This talk presents an approach where grammars can be used as libraries for new grammars and for programs that involve natural language components. The approach is implemented in GF (Grammatical Framework), which is a special-purpose functional programming language for writing grammars. Several features of GF are used in an essential way: the division between abstract and concrete syntax; the module system, including parametrized modules; the type system, which is able to enforce grammar checking via type checking; and code generation that makes GF grammars usable in other programming languages, such as C, Haskell, and Java. To bring the discussion to concrete level, we introduce the GF Resource Grammar Library, which implements the basic grammars of ten languages and makes them accessible to non-linguist application programmers. As an application, we show how the library can be used in building a natural-language interface to a proof system.

Tuesday 5th December 2006 at 14h Patrick Thévenon
Soutenance de thèse : Vers un assistant de preuve en langue naturelle

Abstract: (Hide abstracts)
Cette Thèse est la conclusion de trois ans de travail sur un projet nommé DemoNat. Le but de ce projet est la conception d'un système d'analyse et de vérication de démonstrations mathématiques écrites en langue naturelle. L'architecture générale du système se décrit en 4 phases : 1. analyse de la démonstration par des outils linguistiques ; 2. traduction de la démonstration dans un langage restreint ; 3. interprétation du texte traduit en un arbre de règles de déduction ; 4. validation des règles de déduction à l'aide d'un démonstrateur automatique. Ce projet a mobilisé des équipes de linguistes et de logiciens, les deux premières phases étant la tâche des linguistes, et les deux dernières étant la tâche des logiciens. Cette thèse présente plus en détail ce projet et développe principalement les points suivants : - définition du langage restreint et de son interprétation ; - propriétés du type principal de termes d'un lamlbda-calcul typé avec deux flèches entrant dans le cadre d'un outil linguistique, les ACGs ; - description du démonstrateur automatique.

Thursday 30th November 2006 at 14h Frédéric Ruyer
Soutenance de thèse : Preuves, Types et Sous Types

Abstract: (Hide abstracts)
Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST développé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types en se basant sur des treillis complets comportant des propriétés additionnelles permettant d'interpréter types et termes;puis nous étudions diverses propriétés théoriques du système telles que la réduction du sujet ainsi que son expressivité à travers des exemples traitant de la possibilité ou de l'impossibilité de définir des notions-clés de la logique et de l'informatique théorique. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches issus de l'informatique dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

Thursday 30th November 2006 at 10h15 Gilles Dowek
Les algèbres de valeurs de vérités et la normalisation

Abstract: (Hide abstracts)
On propose une notion de modèle pour la logique intuitionniste, qui étend celle fondée sur les algèbre de Heyting. Cette notion de modèle permet de distinguer l'équivalence logique (si A est démontrable, alors B aussi, et vice-versa) de l'équivalence calculatoire (toute démonstration de A est une démonstration de B, et vice-versa), ce que ne permettaient pas de faire les algèbres de Heyting. On montre ensuite que cette notion de modèle peut être utilisée pour démontrer la normalisation des démonstrations dans de nombreuses théories comme l'arithmétique de Peano ou la logique d'ordre supérieur.

Thursday 16th November 2006 at 10h15 K Ranalter
Categories for Pragmatics

Abstract: (Hide abstracts)
In this talk we present a categorical proof theory for a logic for pragmatics. The aim of this logic is to provide a framework that allows to formalize reasoninig about the pragmatic force with which a sentence may be uttered. The concept of pragmatic force comes from speech act theory and plays a crucial role also in certain branches of artificial intelligence, in particular in the developement of communication protocols for software agents. Instead of considering the full-blown theory of speech acts we focus here on speech acts that either have the pragmatic force of an assertion or the pragmatic force of an obligation, and on how these speech acts can be related to each other. In particular, we are interested in a principle proposed by Bellin and Dalla Pozza that allows the propagation of obligations through causal chains of assertions. The study of such principles from the point of view of categorical proof theory is a nontrivial task and we discuss some of the issues that need to be considered in order to get soundness and completeness results.

Thursday 26th October 2006 at 10h15 P Hyvernat
Introduction aux jeux de Conway et nombres surréels ; problèmes de combinatoire.

Abstract: (Hide abstracts)
Conway a grandement participé à l'élaboration de la théorie des nombres surréels et à la théorie des jeux à deux personnes. Rapidement, un nombre surréel peut-être vu comme un jeu (potentiellement infini) très inintéressant. À cause de cette différence, les deux théories se sont depuis développées de manière quasi indépendante. Je présenterais d'abord le noyau commun aux nombres surréels et aux jeux. Ceci expliquera notamment comment il est possible d'obtenir la moitie d'un coup d'avance sur son adversaire. (Obtenir un tiers de coup d'avance est nettement plus complexe !) Je passerais ensuite à la théorie des jeux impartiaux (style Nim) dont la théorie, plus ancienne, est comprise dans la précédente. Le but est de présenter (prouver ?) le théorème de Sprague-Grundy ainsi que la conjecture sur les jeux octaux. Si le temps et l'assistance le permettent, je présenterai les avancées récentes autour des jeux impartiaux où l'on inverse gagnant et perdant (convention de 171 misère 187). Pour les survivants, je pourrais même parler (peut-être pendant le repas) de la catégorie de jeux due à André Joyal : c'est probablement la toute première catégorie monoidale close de jeux / stratégies. (Malheureusement, elle ne permet pas de modéliser la logique linéaire...) Je ne présenterais rien de nouveau dans cet exposé. Il s'agit en quelque sorte d'une publicité vantant les joies insoupçonnées de la combinatoire des jeux. Idéalement, une ou deux personnes auront envie de m'accompagner pour aller regarder un peu plus loin...

Thursday 19th October 2006 at 10h15 travail collectif
groupe de travail sur un resultat de Gandy

Abstract: (Hide abstracts)
Nous chercherons à comprendre la preuve de forte normalisation du lambda calcul simplement typé (et de certaines extensions : système T de Godel, ajout d'un produit, ...) faite par Gandy. Il semble que cette preuve utilise une mesure (entière ?) qui décroit par réduction.

Thursday 12th October 2006 at 11h Aurelien Pardon
Une explication du critere de Danos-Regnier pour MLL

Abstract: (Hide abstracts)
Les représentations graphiques des preuves de la logique linéaire, les proof-nets, permettent de s'abstraire de contraintes inhérentes au calcul des séquents comme la syntaxe et les règles structurelles. La correction (ou prouvabilité) de tels réseaux peut se vérifier à l'aide de critères purement graphiques, comme le critère de Danos-Regnier. Sa simplicité en fait le rend très efficace mais peu compréhensible. Pour donner une preuve de complétude d'un tel critère et tenter de l'expliquer, nous utiliserons une logique différente : MILL. Dans ce système intuitionniste, les règles logiques sont des règles de typage d'un lambda-calcul et les réseaux de preuves ses arbres de syntaxe. Le critère de Danos-Regnier nous permettra de construire un lambda-terme typable à partir du réseau de preuve, assurant ainsi sa validité.

Thursday 5th October 2006 at 10h15 F Becker
Pavages auto-assemblants : un calcul géométrique

Abstract: (Hide abstracts)
Les pavages auto-assemblants sont un modèle de calcul introduit par Winfree en 2000 afin d'étudier les phénomènes d'auto-assemblage, naturels et artificiels. Je présenterai ce modèle de calcul, d'abord sa définition, puis deux constructions importantes en programmation, le passage paramètre <-> argument (théorème s-n-m) et la récursion, dont nous verrons qu'elles sont assorties de contraintes géométriques pas toujours triviales. Nous verrons ces deux notions appliquées dans des jeux de tuiles simples, l'un qui implémente les homothéties, et l'autre qui assemble le pavage de Robinson (un pavage quasi- périodiques). Nous examinerons aussi les limites du modèle, qui sont de deux sources, l'une géométrique, avec des problèmes de type dead-lock qui rappellent le parallélisme, l'autre rattachée à la complexité Turing. Si le temps le permet, je présenterai des idées de graphes de Cayley qui permettent de s'affranchir de ces limites.

Thursday 28th September 2006 at 10h15 G Theyssier
Automates cellulaires et systèmes dynamiques

Abstract: (Hide abstracts)
Dans cet exposé, je parlerai des automates cellulaires vus comme des systèmes dynamiques et sous l'angle de propriétés topologiques classiques comme la (non-)sensibilité aux conditions initiales et l'expansivité. Je présenterai la classification de Kurka basée sur ces propriétés dans la topologie de Cantor et son interprétation en terme de circulation de l'information. Cette classification a le défaut de ne pas être invariante par décalage ce qui la rend artificielle pour les automates cellulaires. Le reste de l'exposé sera consacré à une approche récente pour résoudre ce problème : reprendre les différents modes de circulation de l'information de cette classification mais en les étendant à toutes les directions dans l'espace-temps. Cette dernière partie contiendra des résultats de M. Sablik mais aussi une petite collection de questions ouvertes.

Thursday 21st September 2006 at 10h15 Christophe Raffalli
PhoX et après ?

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

Thursday 29th June 2006 at 10h15 Karim Nour
Une sémantique de réalisabilité pour un système de type avec intersection et variables d'expansion.

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

Thursday 22nd June 2006 at 10h15 Noel Bernard
Introduction aux Bigraphes

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

Thursday 15th June 2006 at 10h15 François Régis Sinot
Stratégies du lambda-calcul dans les réseaux d'interaction

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

Thursday 8th June 2006 at 10h15 Laurent Vuillon
Combinatoire et mots de Sturm

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

Thursday 11th May 2006 at 14h Laurent Regnier (Université de la Méditerranée),
TBA

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

Thursday 27th April 2006 at 10h Olivier Laurent (en cours de negociation)?
TBA

Abstract: (Hide abstracts)

Thursday 13th April 2006 at 10h15 Khelifa Saber
Un résultat de complétude pour une classe de types du système F

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

Thursday 6th April 2006 at 10h15 Hugo Herbelin
Au coeur de la dualité du calcul : appel par nom, appel par valeur et calcul des séquents

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

Thursday 30th March 2006 at 14h Julien Moncel
Identification de sommets dans les graphes. (Attention : 14h)

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

Thursday 30th March 2006 at 10h15 Guillaume Theyssier
Automates cellulaires : de l'objet syntaxique au système dynamique

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

Monday 27th March 2006 at 10h15 Olivier Brunet
Éléments d'une logique de la connaissance quantique (Attention, c'est un lundi)

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

Thursday 23rd March 2006 at 14h15 Julien Forest
Réécriture d'ordre supérieur avec motifs. (Attention : 14h15)

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

Thursday 16th March 2006 at 10h15 Nicolas Bedaride
Complexité du billard polyédral

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

Thursday 9th March 2006 at 10h15 Emmanuel Beffara
Modèles concurrents de la logique linéaire

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

Thursday 9th February 2006 at 14h Yves Guiraud
Polygraphes, réécriture et logique (Attention : 14h)

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

Thursday 2nd February 2006 at 14h Damien Jamet
Combinatoire des mots en géométrie discrète (Attention : 14h)

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

Thursday 19th January 2006 at 10h Pierre Hyvernat (Institut mathématique de Luminy),
Programmation, simulations, topologie et types dépendants (and much more if time permits)

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

Thursday 12th January 2006 at 10h15 Katell Morin-Allory
A proof of correctness for the construction of property monitors

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

Thursday 5th January 2006 at 10h15 Peter Battyanyi
Weak normalization of the Lambda mu calculus with the rules mu' and rho

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

Seminars of team LIMD

Year 2006