En caml, le typage statique permet de garantir que les programmes bien typés s'exécutent sans erreur de mémoire : jamais votre programme caml, s'il existe, ne confondra un entier avec un pointeur, et jamais un pointeur ne pointera dans le vide ! Ainsi, et par opposition aux langages à typage dynamique, il n'est pas nécessaire de conserver les types à l'exécution, ce qui est un énorme gain de temps et d'espace. Mais cette absence d'information de type devient un handicap dès qu'il s'agit de définir un mécanisme générique pour exporter, puis ré-importer, des valeurs vers un fichier, un réseau — ou dès qu'il s'agit d'interopérer avec d'autres langages de programmation —; car dans ces deux cas une vérification dynamique de type peut-être nécessaire.

Dans cet exposé, je présenterai les vérifications dynamiques de type qu'il est possible et utile de faire dans un programme caml sans pour autant encombrer la mémoire d'inutiles informations de type.

Introduits par Girard dans les années 1980, les réseaux de la logique linéaire forment un langage de programmation qui représente une théorie mathématique des fonctions.

En mathématiques, la notion de linéarité est très importante. Cette notion existe en informatique. Mais à première vue, elle n'a pas la même signification : un terme est dit linéaire s'il utilise exactement une fois son argument. Cependant, il existe de nombreuses analogies entre les deux notions. Ainsi, on peut modéliser les réseaux de la logique linéaire en utilisant des fonctions (développables en séries entières) entre espaces vectoriels.

Le calcul différentiel permet d'obtenir la meilleure approximation linéaire d'une fonction. T. Ehrhard et L. Regnier ont défini les réseaux différentiels en ajoutant des constructeurs différentiels qui permettent de linéariser les réseaux de la logique linéaire à travers le développement en série de Taylor.

Cet exposé débutera par une présentation succincte des réseaux de la logique linéaire puis de leur version différentielle. Il se poursuivra par une étude du développement de Taylor des réseaux de la logique linéaire.

Toutes les deux semaines au séminaire thésard quelqu'un raconte une jolie histoire. Certains comptent les moutons ou coupent des triangles en trois. Certains jours, on joue avec des catégories ou bien on joue à des jeux de hasard mais pendant longtemps, très longtemps. Et bien sûr il y a l'inépuisable livre d'histoires de la dynastie des lambdas.

Moi, j'ai choisi d'écrire mon histoire avec un alphabet infini. L'avantage c'est qu'avec une histoire très courte, on peut déjà raconter des choses très compliquées. Mais encore faut-il que les gens puissent comprendre et ou au moins apprécier la beauté de ces histoires.

Dans cet exposé, je vous montrerai comment écrire des mots et dessiner des arbres avec un alphabet infini. Je vous expliquerai ensuite dans quelle mesure et avec quels outils théoriques on peut caractériser et manipuler ce type de langages.

Nous allons bien nous amuser tous ensemble, en découvrant le monde magique et merveilleux des sémantiques de jeux. Les sémantiques de jeux ont été introduites pour capturer le comportement interactif des preuves en interprétant les formules par des jeux sur lesquels les preuves induisent des stratégies. Nous proposons ici un modèle de jeux de la logique propositionnelle du premier ordre sans connecteurs. L'une des difficultés majeures lors de la définition de telles sémantiques, est de les rendre précises, c'est-à-dire de caractériser les stratégies définissables (qui sont l'interprétation d'une preuve). Cette caractérisation est habituellement faite en se restreignant à des stratégies qui vérifient certaines conditions, l'innocence par exemple. Dans ce travail, nous proposons une méthode originale pour effectuer cette caractérisation en introduisant une présentation des stratégies définissables : nous montrons qu'elles peuvent être engendrées à partir de stratégies « atomiques » en nombre fini et que l'égalité entre les stratégies engendrées de la sorte est finiment axiomatisable. Bravo à tous ceux qui sont arrivés jusque là, ça sera vachement plus drôle mercredi, c'est promis.

Si un jour vous vous ennuyez, vous pouvez dessiner un triangle et vous mettez un point au milieu que vous reliez a chacun des sommets, du coup vous avez trois petits triangles. Vous en choisissez un (de manière aléatoire sinon c'est pas rigolo) et vous recommencez. Si vous vous ennuyez vraiment beaucoup vous allez finir par obtenir une sorte de triangle avec plein de petits triangles dedans et ca les gens qui veulent se la raconter appellent ça une triangulation en pile. Après vous pouvez essayer de regarder un peu la tête qu'elle a genre quelle est la longueur d'un chemin entre deux points ou ce genre de choses.

Et puis après vous pouvez venir raconter ça au séminaire thésard en faisant plein de dessins et en agitant beaucoup les bras et en faisant que des probas super fastoches.

CPC (Continuation Passing C) est un transformateur de programmes qui transforme un programme écrit en un C augmenté de primitives de concurrence en C séquentiel. Ce faisant, il transforme un programme écrit en un style « processus légers » en un programme à événements, plus efficace.

Après avoir évalué les performances de CPC sur un exemple concret (serveur web), nous détaillerons son fonctionnement et étudierons la correction des transformations effectuées. Nous nous attacherons plus particulièrement au cas du lambda-lifting de variables impératives.

Travail réalisé avec Hugo Gimbert (LaBRI)

Les jeux stochastiques constituent un modèle naturel pour la synthèse de contrôleurs en milieu ouvert, lorsque certaines actions peuvent être considérées comme aléatoires. Deux questions majeures se posent :

• Peut-on garantir une propriété quasi-sûrement ?
• Si non, avec quelle probabilité peut-on la garantir ?

Le second problème est nettement plus complexe que le premier. En particulier, pour le cas de base des jeux d'accessibilité, le problème quasi-sûr est polynomial, tandis que le problème optimal est dans NP ∩ co-NP.

Dans cet exposé, je présenterai les deux attaques classiques de ce problème : par valeurs et par amélioration de stratégies. Je présenterai ensuite un angle d'attaque original, manipulant des ordres sur les états aléatoires du graphe, ainsi que différents algorithmes qui en dérivent. En particulier, je montrerai comment nos résultats peuvent s'adapter à toutes les conditions de victoire préfixes-indépendantes, à travers un méta-algorithme liant directement la complexité du calcul des valeurs à celle des problèmes quasi-sûrs et à un seul joueur.

Pour simplifier la gestion de leurs differents composants, la plupart des distributions de logiciel libre ont mis en place un système de paquetage, qui permet d'ajouter des données aux composants de la distribution pour pouvoir les traiter d'une façon unifiée. Ces « meta-données » concernent donc les specificités des composants, par exemple leur contenu, leur licence, leurs options de compilation, et aussi leurs dépendances.

Dans cet exposé, je voudrais présenter le travail des projets EDOS et Mancoosi sur la vérification automatique de ces distributions.

La décomposition modulaire est une décomposition de graphes qui a été très étudiée aux cours des dernières décennies. Elle a été introduite pour la première fois par T. Gallai en 1967, et redécouverte à plusieurs reprises notamment en sciences sociales, et en bio-informatique.

Dans cet exposé nous rappellerons la définition et les propriétés intéressantes de la décomposition modulaire. Nous montrerons ensuite comment le concept de casseur permet d'étendre cette dernière à d'autres structures que les graphes. Pour ce faire nous introduirons les relations homogènes, structure qui généralise les graphes.

Nous présenterons également une nouvelle décomposition, celle-ci appellée umodulaire, et présenterons les premières propriétés de cette dernière. Qui fournit une toute nouvelle décomposition des tournois.

L'assistant de preuves Coq permet la génération de programmes corrects par construction. Cette fonctionnalité, appelée extraction, est de plus en plus exploitée pour produire des bibliothèques de fonctions certifiées, voire des programmes tout entier. Ainsi, un compilateur d'un sous-langage du C a été développé avec Coq, et un compilateur pour langage fonctionnel est en cours. Cependant, l'extraction elle-même n'est pas certifiée.

Dans cet exposé, je présenterai deux approches pour certifier l'extraction : l'extraction certifiée, et la certification extraite.

En combinatoire on aime bien compter et donner des noms aux objets qui n'ont aucun rapport avec ce qu'ils sont.

Alors je vais vous expliquer comment on peut compter des animaux mais avant il faudra que j'explique ce que c'est un animal et puis un gaz aussi parce qu'on s'en sert pour compter les animaux.

C'est les physiciens qui ont appelé un gaz un gaz, ça non plus je sais pas trop pourquoi mais je vous dirai quand meme ce que c'est. Et puis j'expliquerai un peu de probabilités parce qu'au final les animaux et les gaz c'est sympa mais quand ils sont aléatoires c'est plus rigolo.

Les réseaux d'interaction forment un modèle de calcul local parallèle et confluent. Nous introduirons un système d'opérateurs dans ce formalisme qui permet de coder les termes de la logique linéaire (enrichie d'un let rec) en des réseaux. Ces réseaux seront considérés comme du bytecode dont l'exécution est réalisée par application de certaines règles de réduction. La machine d'exécution utilisée pourra tirer parti de la capacité de parallélisation très fine de ce système de réduction. La partie difficile est celle qui consiste à localiser le calcul des boîtes (exponentielles et additives) que l'on trouve dans les réseaux de preuve.

Le π-calcul est un langage formel qui décrit l'interaction entre les processus. Les processus représentent aussi bien les processus légers (threads) ou les processus (lourds). On présentera rapidement le π-calcul. Puis, de façon plus détaillée, le Sπ-calcul qui est une version synchrone du π-calcul, basé sur le modèle synchrone SL.

Dans cet exposé, on s'intéressera aux notions de déterminisme et confluence dans le Sπ-calcul. Et on verra un système de typage qui garantit le déterminisme.

Je présenterai dans l'exposé un modèle pour l'évolution des génomes (représentés comme des permutations d'un ensemble de gènes) qui s'appuie uniquement sur le phénomène biologique de duplication-perte, souvent mis de côté dans les modèles classiques. Je montrerai d'abord comment on peut interpréter les résultats obtenus par les auteurs ayant défini ce modèle, afin de caractériser les permutations obtenues après p étapes de duplication-perte. Cette caractérisation se formule en termes de motifs exclus dans les permutations. J'étudierai ensuite une variante du modèle, en essayant de résoudre les mêmes questions algorithmiques et combinatoires que dans le modèle précédent : quel est le nombre C d'étapes nécessaires pour obtenir une permutation donnée ? peut-on décrire un algorithme qui calcule une suite de C étapes pour obtenir cette permutation ? y a-t-il une caractérisation par motifs exclus des permutations obtenues après p étapes dans ce modèle ? (Éléments de) réponse le 21 novembre...

Le λ-calcul se fait vieillot (années 30) et souffre de plusieurs défauts. L'un de ceux là est que la règle de réduction (β) fait intervenir une opération de substitution non définie dans le langage, ce qui laisse une liberté lors de l'implémentation et donc conduit à des bugs (même en Coq !).

L'idée est de coder l'opération de substitution dans le langage en la rendant explicite. Mais plutôt que de s'en tenir là, on va également rendre explicites l'affaiblissement et la contraction. Et pour corser le tout, on va paramétriser pour avoir explicite juste un constructeur ou plusieurs.

Ceci donne un cube avec 8 langages dont certains déjà connus (de moi en tout cas) comme le λ-calcul, λ-lxr, λ-es, … et d'autres nouveaux. C'est ce que cube que j'ai formalisé et étudié durant mon stage de DEA et je vais vous parler des propriétés (nombreuses) qu'il satisfait.

L'exposé sera simple et nos résultats ne seront pas exprimés par les mots clés habituels du jargon (ou presque). Pour donner envie aussi aux personnes qui veulent avoir mal la tête, je toucherai deux mots de l'hypercube…

Les automates à pile (PDS) sont couramment utilisés pour la modélisation des programmes séquentiels avec appels de procédures (1-thread) et plusieurs algorithmes ont été proposés pour résoudre l'accessibilité. La question est comment étendre ces techniques pour la vérification des programmes concurrents.

Récemment, K. Sen et M. Viswanthan ont proposé le « Multiset Pushdown System » (MPDS) pour modéliser les programmes concurrents avec des appels de procédures et la création dynamique de tâches asynchrones. Un MPDS est un PDS auquel on rajoute un sac (multiset) qui contient des tâches en attente d'être exécutées. Durant le traitement d'une tâche, le PDS pourra créer de nouvelles tâches qui vont se rajouter au multiset. Lorsque sa pile redevient vide, le PDS prend d'une manière non-déterministe une autre tâche du multiset et commence à l'exécuter.

Dans cet exposé, je vais vous rappeler comment résoudre le problème d'accessibilité d'un PDS, introduire le modèle MPDS et présenter un algorithme pour décider l'accessibilité pour ces systèmes.

Le λ-calcul est un langage formel très simple par sa syntaxe, mais d'une grande expressivité: théoriquement, toute fonction récursive est exprimable par un λ-terme. Cependant en pratique, il est souvent nécessaire d'utiliser des codages relativement lourds. Afin de rendre ce calcul plus facilement manipulable, différentes extensions ont été développées. Une des extensions importantes est le filtrage (pattern matching en anglais), utilisé notamment dans les langages de programmation fonctionnelle, comme CAML.

Je présenterai dans cet exposé une des extensions du λ-calcul modélisant le filtrage: le λ-calcul avec constructeurs. Je proposerai aussi un système de type pour ce calcul, sur lequel j'ai travaillé durant mon stage de DEA, et j'évoquerai quelques propriétés intéressantes qu'il satisfait.

Les jeux constituent un objet d'études intéressant à plus d'un titre. En effet, outre les applications en vérification, synthèse, et autres modèles logiques — qui nous permettent de voyager à l'oeil —, ils constituent une réponse socialement correcte⁰ à l'éternelle question "Et alors, c'est quoi que tu cherches¹ ?".

Dans ce cadre, un problème classique consiste alors à convaincre l'interlocuteur que l'on fait un vrai boulot sérieux. La réponse canonique au LIAFA invoque des parties de durée infinie, mais de plus en plus de gens ne sont pas convaincus qu'il s'agit là d'une réponse à la fois adaptée et auto-suffisante, et continuent à poser des questions. Dans ce travail commun avec Florian Horn, nous avons imaginé un moyen de donner mal à la tête même à ces fâcheux, en passant d'un infini (trop) simple à toute une hiérarchie d'infinis successifs et emboîtés.

Dans cet exposé, je montrerai comment essayer de donner une motivation pratique qui tient à peu près la route, avant d'expliquer la manière de résoudre ce genre de jeux sans trop d'efforts supplémentaires. Nos résultats sont exprimés par les mots clés habituels du jargon, avec les indispensables utilisations de fontes typewriter.