Les systèmes de types purs sont un bon moyen d'obtenir des résultats généraux sur des familles de lambda-calculs typés comme le Lambda Cube de Barendregt. Néanmoins, essayer d'étendre ce formalisme à autre chose que la seule Beta-réduction peut s'avérer périlleux.

Dans une première partie, je presenterai ce que sont ces PTS(pure type system) et le genre de résultats que l'ont peut obtenir. Puis, je m'interesserai plus particulierement à la réduction utilisée dans ces PTS, en voulant ajouter la regle Eta, et ainsi mettre en evidence les problèmes qui lui sont liés. Je présenterai enfin les différentes pistes qui ont été mise en oeuvre pour essayer de résoudre ces problèmes, et plus particulierement celle qui passe par une nouvelle forme de PTS, proche du calcul des sequents.

PS: Le tout est bien sur prouvé en Coq, on est jamais trop prudent.

Ça parlera de graphes augmentés et des deux protocoles routage et diffusion. Après une présentation plus ou moins longue des protocoles, je mentionnerai une partie des résultats plus ou moins récents afin de comparer ces protocoles.

Nous présenterons le modèle probabiliste de k-SAT et nous verrons quel genre d'informations ce modèle peut apporter quant à la complexité algorithmique du problème k-SAT. En particulier nous verrons pourquoi P != NP ).-|-|-|-(

L'analyse des réseaux sociaux a longtemps été un courant de recherche principalement associé aux sciences sociales avant de connaître un regain d'intérêt dans la décennie précédente : le développement du Word-Wide Web et la possibilité de disposer de très grands jeux de données ont alors permis la création d'un nouveau champ de recherche à partir de la découverte des propriétés que partagent un grand nombre de grand réseaux qui sont issus de domaines aussi variés que la biologie, l'économie, la linguistique et bien sûr la sociologie ou l'informatique.

Ce sont ces réseaux que l'on appelle « complex networks » ou « petits mondes ». L'originalité de ces réseaux est qu'ils ne sont pas définis formellement : ils sont généralement connus à travers une opération de mesure et leur très grande taille impose des contraintes importantes dans l'élaboration des algorithmes destinés à les traiter.

À partir des fils de commentaires du site Flickr, nous allons nous intéresser à la manière dont un grand réseau social évolue au fil du temps, et en particulier comment les individus qui le composent se rencontrent et constituent peu à peu leur entourage.

La théorie de la preuve est la branche de la logique qui a compris que savoir si on peut prouver un théorème est à peu près aussi intéressant que de savoir qu'on peut finir Megaman 9. En crédit : elle s'intéresse aux preuves en tant qu'objets, et à leur dynamique, pas à la prouvabilité. Ce qui nous intéressera dans cet exposé est la manière dont on représente ces objets, c'est-à-dire le formalisme logique dans lequel on se place.

Je vais rapidement présenter la tradition dans ce domaine, formée par les deux principaux formalismes, introduits par Gentzen en 1934. Le premier, la déduction naturelle, a connu le succès grâce à l'isomorhpisme dit de Curry-Howard (dont les cultistes sont très nombreux aujourd'hui). Le second sera plus important pour nous : le calcul des séquents est la référence dans ce domaine, l'outil privilégié quand on veut faire de la vraie science avec des vraies preuves.

Mais la crise est passée par là, car les idées modernes de concurrence, de dynamique et de géométrie s'accommodent mal des contraintes du calcul des séquents. Alors on essaye de faire mieux, et ça marche un peu, notamment depuis l'introduction des proof-nets par Girard en 1986. Cette vision moderne des preuves a beaucoup fait évolué le domaine, et c'est maintenant un sujet très étudié (et puis ça fait des jolis dessins).

Mais c'est sur une autre vision de la modernité en théorie de la preuve que je vais me concentrer. Il s'agit de la méthodologie nommée "inférence profonde", et de son principal formalisme, le calcul des structures, introduit par Guglielmi en 99. Je présenterai celui-ci plus en détail, en essayant d'illustrer l'idée qui le sous-tend : revenir à une forme plus primitive pour avoir une meilleure granularité dans l'étude des preuves (évidemment, ça se paye en terme de complexité, et c'est pas donné). À la fin, on essaiera de prendre un peu de recul et de voir où tout ça, la tradition et la modernité, peut nous mener.

Dans cet exposé, on va montrer comment des conditions de gains sur des graphes peuvent aussi servir à faire des *vrais* jeux (spéciale dédicace à Florian Horn). On va partir des définitions habituelles de sémantique des jeux, et les enrichir par des conditions de gain. On considèrera alors des stratégies gagnantes, et on montrera qu'elles correspondent aux preuves d'un calcul des séquents étendu par des constructions pour des types inductifs et coinductifs (i.e. inductifs en changeant le sens des flèches). Si ça ne vous a pas convaincus, il y aura aussi un petit déjeuner.

Au fur et à mesure de besoins de l'exposé, je définirai les classes de permutations, leurs bases, les séries génératrices, les arbres de décomposition, les permutations simples, et autres objets combinatoires qui s'inviteront au séminaire des thèsards.

Pour ce qui est du contenu principal de l'exposé, on étudie la classe des « pin-permutations » (ou permutations en épingles) qui sont celles possédant une représentation en épingles. Cette classe a été définie récemment dans une série d'articles de Brignall et al., où elle est utilisée pour rechercher des propriétés d'autres classes de permutations (algébricité de la série génératrice, décidabilité de l'appartenance à la classe), en fonction des permutations simples contenues dans ces classes. On donne une caractérisation des arbres de décomposition des permutations en épingles, qui nous permet de calculer la série génératrice de cette classe, prouvant ainsi la conjecture de Brignall concernant le caractère rationnel de cette série génératrice. En outre, on prouve que la base de la classe des permutations en épingles est infinie.

Ça a l'air un peu barbare dit comme ça, mais il y a plein de jolis dessins !

Multiset pushdown systems have been introduced by Sen and Viswanathan as an adequate model for asynchronous programs where some procedure calls can be stored as tasks to be processed later. The model is a pushdown system supplied with a multiset of pending tasks. Tasks may be added to the multiset at each transition, whereas a task is taken from the multiset only when the stack is empty. In this paper, we consider an extension of these models where tasks may be of different priority level, and can be preempted at any point of their execution by tasks of higher priority. We investigate the control point reachability problem for these models. Our main result is that this problem is decidable by reduction to the reachability problem for a decidable class of Petri nets with inhibitor arcs. We also identify two subclasses of these models for which the control point reachability problem is reducible respectively to the reachability problem and to the coverability problem for Petri nets (without inhibitor arcs).

This is joint work with Ahmed Bouajjani and Tayssir Touili.

Vous vous êtes toujours demandé ce qu'était PAF! et comment ça marchait, n'est-ce pas ? Eh bien, votre curiosité va bientôt être satisfaite. Comme vous êtes sûrement en train de trépigner d'impatience, voilà un petit avant goût:

PAF! est un assistant à la preuve dédié au fragment fonctionnel de ML, Le but de cet assistant est de permettre à l'utilisateur de prouver l'adéquation d'un programme fonctionnel vis-à-vis d'une spécification donnée, sans restriction sur les formes de récursion utilisées, autorisant ainsi le raisonnement sur les fonctions partielles et/ou définies par récursion non structurelle. Le moteur de preuve de PAF! est fondé sur une logique multi-sortée du second ordre à la AF2 dont les objets de base sont les programmes fonctionnels (avec récursion non gardée). Le principal ingrédient du langage de spécification est un prédicat de typage fort, p↓T, qui exprime la correction forte du programme p vis-à-vis du type T (laquelle implique notamment la terminaison de ce programme dans tous les contextes appropriés à son type).

Essentiellement, je présenterai le formalisme de PAF! (pour ceux qui n'aiment pas le calcul des séquents, c'est raté…), je dirai un mot de la preuve de sa cohérence et peut-être que je ferai une démo en live (mais ça c'est pas sûr).

Beaucoup de variantes du problème d'ordonnancement de n tâches existent, les unes décidables, les autres non. Notre but est donc de proposer une modélisation permettant de prendre en compte toutes ces variantes, avec leurs conditions, et de mieux cerner la limite entre décidabilité et indécidabilité dans ce domaine. Nous avons donc choisi de modéliser les tâches et les stratégies d'ordonnancement par des automates temporisés, qui nous permettent de nous ramener à un « simple » problème d'accessibilité.

Au programme : des automates, une zoologie, et quelques petits exemples ludiques.

Pour les appels de fonctions en OCaml, les arguments sont en général évalués avant le corps de la fonction. On perd la terminaison de quelques programmes, mais on garde l'adéquation avec une théorie de l'exécution relativement simple.

Cependant, cette théorie possède certaines « failles », qui correspondent à l'exécution de programmes compilés mais pas linkés. On parlera donc un peu de ces problèmes, de ce qu'on aimerait qu'il se passe et de deux solutions à tout ça.

Multithreaded programs (with procedure calls, thread creation, global/local variables over infinite data domains, locks, monitors, etc.) form a large class of programs, challenging from the verification point of view.

In this talk, I'll describe a general framework for reasoning about these programs. We consider that configurations of such programs are represented by nested data words, i.e., words of … words over a potentially infinite alphabet. We define a logic allowing to reason about nested data words. The formulas of these logic are going to be used to describe the properties of the program to verify.

If you didn't appreciate the abstract above, then you can consider that the presentation will contain some logical formulas… and hopefully enough pictures to explain the formulas.

The presentation will give an introduction to the theory of elementary toposes, aimed towards logicians and computer scientists.

Category theory allows a more conceptional view on basic mathematical constructions (such as cartesian products) than set theory. Surprisingly few of these basic constructions suffice to capture what happens in mathematical practice. A category in which these constructions can be carried out is called an elementary topos. Thus, topos theory may be viewed as a conceptually clearer alternative to set theory.

However, whereas set theory is usually seen as canonical, there are many different toposes, each constituting its own mathematical universe. An intriguing feature of a topos is that logic is internalized: even if we work with normal ‘classical’ logic externally, inside a specific topos, the axiom of choice and even the principle of proof by contradiction may fail.

In the presentation, I will give a precise definition of elementary topos, and then state some easy examples. If there is time, I will give an informal account of the internal logic.

Les règles métier (en anglais business rules) sont un concept qui date de la Haute Epoque de l'intelligence artificielle. Un des graals de l'I.A. était, rappelons-le, de parvenir à faire reproduire par un ordinateur les raisonnements humains dans un domaine donné. Pour arriver à cette fin, un Ingénieur Cogniticien se livrait à un Recueil d'Expertise auprès d'un Expert Métier. Il en résultait un programme informatique (le Système Expert) qui incarnait le savoir de la branche d'expertise en question. Ce programme était classiquement écrit dans un langage à base de règles, le plus connu étant Prolog.

Quelques décennies et krachs boursiers plus tard, ces idées n'ont pas complètement disparu. Elles se sont réincarnées sous une nouvelle terminologie, avec des objectifs moins grandioses, mais non moins réels. Ainsi chaque transaction VISA ou Mastercard, chaque mise en vente eBay, chaque demande de crédit chez China Everbright Bank, chaque réglage de pacemaker chez St-Jude Medical... passe par un programme de règles.

Mais... vous avez dit programme ? Vous avez donc dit bug ! Et aussi vérification de programme. Dans cet exposé, je regarderai ce qui est commun et original dans la vérification de programmes de règles métier.

Informatique : nom féminin, science du traitement automatique et rationnel de l'information considérée comme le support des connaissances et des communications. Fin de la citation Larousse, le fond concret de l'affaire est qu'on tripote des données.

Mais il y a une chose qu'on a remarquée depuis longtemps en algorithmique : si lesdites données sont organisées comme il faut, alors on gagne du temps. C'est comme de ranger son bureau, sauf que ça marche pour de vrai. On s'est donc mis à donner des formes spécifiques à l'ensemble selon l'usage qu'on voulait faire des données. Et c'est là que les problèmes arrivèrent. Chacun se mit à écrire des programmes spécifiques, pour les jeter à la poubelle et recommencer au moindre coup de peinture dans un coin de la forme.

Heureusement, ceci n'est pas une fatalité. On explorera quelques idées qui permettent de programmer en se jouant de l'organisation des données, et d'autres jeux plus complexes entre fond et forme.