Le lambda-calcul est un langage fonctionnel équivalent aux machines de Turing. L'utilisation de modèles dénotationnels (l'interprétation du lambda-calcul par des objets mathématiques) permet d'étudier certaines de ses propriétés. En effet, ces modèles étant définis pour être compositionnels, c'est-a-dire que les termes sont entièrement définis par leurs sous-termes, cela facilite certaines démonstrations.

Nous verrons donc après certains rappels sur le lambda calcul et une introduction aux notions nécessaires sur les catégories, une application concrète simple grâce au modèle REL.

Les langages réguliers forment une classe largement étudiée dans la littérature. L'équivalence entre automates, logique et monoïdes finis a permit d'obtenir une classification extensive de cette classe ainsi que de ses sous-classes décidables.

Je vous parlerai principalement de logique sur les mots ainsi que de monoïdes finis, puis j'aborderai le thème plus précis que sont les hiérarchies booléennes et donnerai un résultat de décidabilité.

La réalisabilité classique est un moyen d'étendre la correspondance entre preuves et programmes au-delà d'une simple correspondance avec la logique intuitionniste : d'abord à la logique classique, ensuite à la logique classique avec des axiomes non-logiques... Quand cette technologie est appliquée aux axiomes de la théorie des ensembles, elle permet, au passage, de créer de nouveaux modèles de cette théorie, parfois avec des propriétés surprenantes. Même si le plus souvent la réalisabilité classique est étudiée du point de vue de la correspondance entre preuves et programmes, pour l'instant je m'intéresse aux modèles de la théorie des ensembles qui sont ses sous-produits.

Mercredi prochain, je présenterai les algèbres de réalisabilité et une variante de la théorie des ensembles, proposées par J.-L. Krivine. Ensuite j'expliquerai ce qu'est pour un programme de réaliser une formule du premier ordre. A partir de là, j'illustrerai ce que sont les modèles de réalisabilité de la théorie des ensembles, et j'espère finir par donner un exemple de la manière dont l'addition de certaines instructions au langage de programmation permet de pousser ces modèles de la théorie des ensemble à se comporter de manières non-habituelles.

Le model-checking de systèmes à espace d'états finis souffre souvent de l'explosion combinatoire de l'espace d'états. Les systèmes répartis étant la plupart du temps constitués de différents composants avec des comportements similaires, ils présentent des symétries exploitables afin de réduire la taille de l'espace d'états à explorer.

Nous présentons cette technique de réduction par symétries et son utilisation pour le model-checking. Nous indiquerons ensuite des pistes pour combiner cette approche avec des structures de données adaptées à la représentation de "grands" espaces d'états.

Les threads et les événements sont deux techniques classiques pour écrire des programmes concurrents en C. Classiques... mais sûrement pas pour tout le monde.

Ce exposé vous prendra par la main pour vous faire découvrir doucement les mondes merveilleux des threads et des événements, et comment de vaillants bâtisseurs ont construit des ponts de fortune entre les deux.

Mais comme je préfère personnellement les ponts en béton armé, je terminerai en vous présentant CPC (Continuation Passing C), un compilateur source-source transformant des threads en événements : automatisé, efficace et prouvé (à la main, il ne faut pas exagérer).

Le théorème de Bolzano-Weierstrass donne l’existence d'une sous-suite convergente pour toute suite réelle bornée. Mais pouvez-vous donner un algorithme qui avec le code d'une fonction (des entiers dans les rationnels) bornée calculable donne les termes de la sous-suite convergente?

Durant cet exposé nous nous pencherons sur ce type de questions et j'essayerai de faire ressentir en quoi la théorie de la calculabilité permet d'aborder le problème de l'effectivité en mathématiques.

Il existe un formalisme, pour représenter abstraitement un langage de programmation, nommé les algèbres de combinateurs!

Généralement ils sont étudiés pour leur coté combinatoire (créer des points fixes...) voir pas du tout étudiés (un PPSien de base préfèrera faire appel aux catégories, à la programmation pure, ou à des paradigmes étranges comme des domaines ou des jeux).

Et bien ici, pour montrer à nos amis du LIAFA qu'il nous arrive de faire des maths civilisées, je vais en faire une petite étude algébrique.

Nous allons voir que ces algèbres (bien que n'ayant pas d'élément neutre, n'étant pas commutatives et en fait n'étant même pas associatives !!!!), peuvent êtres décomposées en plus petit élément, afin de suivre une étude systématique comme aiment tant le faire les algébristes!

Vous cherchez combien il existe de triangulations d’un polygone convexe à n côtés, de partitions d’un ensemble à n éléments ou d’arbres à n sommets ? La combinatoire analytique résout ces problèmes simplement, sans calcul (ou presque), et fournit des asymptotes.

Son outil principal est la fonction génératrice. Nous verrons comment les spécifications combinatoires des objets se traduisent en opérations sur la série génératrice, puis comment extraire de la série des expressions directes des nombres recherchés ou des asymptotes.

Dans les protocoles de diffusion de types rumeur (gossip protocols) chaque noeud informé du réseau envoie à chaque étape l'information à l'un de ses voisins. Lorsque le choix du voisin se fait aléatoirement (on parle alors de diffusion randomizée) uniformément parmis les noeuds voisins, le protocole est naturellement tolérant aux défaillances et s'adapte facilement à un changement du réseau. De plus la propagation est démontrée rapide avec forte probabilité dans de nombreux graphes. Il a été démontré que le protocole où le choix du voisin se fait suivant une liste donnée par un adversaire mais que l'endroit dont on démarre dans la liste est choisi aléatoirement a généralement les mêmes bonnes propriétés. Je présenterai des résultats sur ce qu'il peut arriver de pire dans ce dernier modèle selon 3 hypothèses différentes :

• SN (skip none) : chaque noeud envoie à chaque étape l'information voisin au suivant dans la liste
• SS (skip sender) : chaque noeud envoie au prochain voisin qui ne l'a pas appellé
• SI (skip informed) : chaque noeud envoie au prochain voisin non informé

Pushdown systems (PDS) are well adapted to model sequential programs with (possibly recursive) procedure calls. Therefore, it is important to have efficient model checking algorithms for PDSs. We consider CTL model checking for PDSs. We consider the "standard" CTL model checking problem where a configuration of a PDS satisfies an atomic proposition or not depends only on the control state of the configuration. We consider also CTL model checking with regular valuations, where the set of configurations in which an atomic proposition holds is a regular language. We reduce these problems to the emptiness problem in Alternating Buchi Pushdown Systems, and we give an algorithm to solve this emptiness problem. Our algorithms are more efficient than the other existing algorithms for CTL model checking for PDSs in the literature. We implemented our techniques in a tool, and we applied it to different case studies. Our results are encouraging. In particular, we were able to find bugs in linux source code.

This is a joint work with Tayssir Touili.

Un automate cellulaire est un réseau régulier de cellules, chacune contenant un état (qui est en général simplement 0 ou 1). Les contenus de toutes les cellules évoluent de manière synchrone, en fonction des états d'un nombre fini leurs voisines.

Le problème de "classification de la densité", qui consiste à chercher un automate cellulaire capable de déterminer si une configuration initiale définie sur un anneau contient une majorité de 0 ou de 1, a fait l'objet de nombreuses recherches. Nous nous intéressons ici à l'extension de ce problème à un réseau infini. Le choix de la configuration initiale est le suivant : pour chaque cellule, on choisit indépendamment d'écrire un 1 avec probabilité p et un 0 avec probabilité 1-p. La question est alors de construire un automate cellulaire qui converge vers la configuration "tout 0" lorsque p est inférieur à 1/2, et vers la configuration "tout 1" quand p est supérieur à 1/2 (synchronisation de toutes les cellules sur l'état majoritaire). Un tel automate cellulaire est dit bifurquer. Nous montrons qu'en dimension 2, l'automate cellulaire de Toom (règle majorité sur le voisinage nord-est-centre) bifurque. En dimension 1, il existe de sérieux candidats pour bifurquer (par exemple l'automate GKL), mais la question reste ouverte.

Les graphes sont des structures de données utilisables pour modéliser une grande variété de problèmes (flots, ordonnancements, etc). Je vous présenterai donc un exposé introductif sur les graphes, la décomposition modulaire, ainsi que sur certaines classes de graphes.

Pollués par des redondances toxiques, nos ordinateurs épuisent leurs ressources à produire des calculs inutiles. Mais par quels moyens et dans quelles conditions peut-on recycler un vieux calcul ?

Nous nous placerons dans le monde de la récriture, où l'on calcule en transformant progressivement une expression jusqu'à obtention d'un résultat. Là, nous mènerons la chasse au gaspi grâce à une analyse des origines et des causes de chaque étape de calcul. Nous en déduirons des méthodes de calcul "vertes", économes en ressources.

Les fonctions de Schur apparaissent partout dans les maths et dans la physique. Les polynômes de Macdonald sont une généralisation des fonctions de Schur avec deux paramètres $q$ et $t$. Je vais expliquer comment voir ces deux objets comme des représentations de groupes symétriques.

I will first introduce the Dynamic Script Language (DSL) which is an orchestration language based on the reactive approach. I will present the formal semantics together with some examples. Then, I will present a possible extension of DSL with the objective to maximize core usage while preserving safety. This extension introduces agents as basic autonomous parallel entities proved free from memory interferences, with help of agents and synchronized schedulers we try to maximize the usage of available cores in this extension.

On considere un reseau de Petri (RdP) markovien avec la "race policy". Le reseau est dit a forme produit si la distribution stationaire peut s'ecrire comme produit des termes qui ne dependent que des marquages locaux. On observe que le theoreme de deficience zero de Feinberg donne un critere simple et structurel pour l'existence de la forme produit. On montre en suite que les RdP a choix libres ayant deficience zero sont les machines d'etats, une version alternative des reseaux de Jackson. Enfin, on donne un ensemble de regles qui permettent de generer tous les RdP a deficience zero.

Des langages comme ML (programmation fonctionnelle), Coq (programmation certifiée) ou encore Java reposent sur une théorie du typage statique qui peut paraître paradoxale.

En effet, si la discipline de typage se doit d'être intuitive, la preuve des propriétés de base des systèmes de typage considérés (préservation du typage par la réduction, etc.) est plus bureaucratique qu'éclairante, et en tout cas est loin de refléter les intuitions initiales.

Derrière les intuitions, cependant, se cachent souvent des mathématiques simples. J'essayerai de vous convaincre que celles des systèmes de typage sont capturées par un outil plus simple que son nom ne le laisse suggérer, et qui nous vient de la logique mathématique: la "réalisabilité classique".

La Logique Temporelle Linéaire (LTL) est souvent utilisée pour spécifier des comportements souhaités par les programmes, ce formalisme offre un bon compromis entre l'expressivité et la simplicité du model-checking. Après une brève présentation de la théorie des fonctions de coût, qui étend la théorie des langages en permettant de compter des évènements dans les mots, on verra comment utiliser LTL pour définir certaines de ces fonctions. On obtient finalement une caractérisation algébrique des fonctions définissables par LTL, ce qui nous permet de décider si une fonction de coût donnée peut être spécifiée de cette manière.

Ἑκάτη (Hekátē) est une déesse grecque chtonienne.

Hekate est un « seeder » BitTorrent écrit en CPC, une extension dotant le langage C de threads très légers.

Ce séminaire sera une balade à travers le code source de Hekate, émaillée de quelques digressions mythologiques. Il vous fera découvrir les plaisirs des threads légers (et polymorphes) et vous donnera, qui sait ?, l'envie de vous (re)mettre au C.

L'arithmétique de Presburger (PA) est la théorie du premier ordre sur les entiers avec l'addition et la comparaison, sa décidabilité fut prouvée par Presburger au moyen d'une méthode d'élimination des quantificateurs. Une version raffinée de cette méthode a été montrée 3EXPTIME, une méthode donc efficace pour décider ce problème montré 2EXPSPACE hard. Nous avons préféré l'approche de Büchi, avec des automates: en représentant les vecteurs d'entiers par des mots, il donne une construction de l'automate acceptant les représentations des vecteurs solutions d'une formule. La force de cette approche, c'est l'obtention d'une representation canonique pour chaque formule de l'arithmétique de Presburger. Je m'attacherai essentiellement à vous présenter cette approche et à vous montrer les résultats que nous avons obtenus.

L'écriture de programmes parallèles, même dans le cas de paradigmes de haut niveau, nécessite généralement des connaissances sur l'architecture matériel utilisée, limitant ainsi à la fois l'adoption de ces techniques de programmation et la portabilité de ces programmes.

Pour réduire ces inconvénients, je présenterai une approche de la parallélisation utilisant des squelettes algorithmiques dans laquelle le parallélisme est entièrement implicite et où le découpage d'un programme en processus distincts ainsi que la répartition de ces processus sur un ensemble de processeurs est effectuée automatiquement.

J'introduis les jeux sur les graphes comme un modèle des systèmes ouverts rencontrés en informatique théorique.

Je prends l'exemple concret d'une imprimante : c'est un système dont la fonction est d'imprimer les documents émis par des utilisateurs. L'exécution des impressions peut être décrite à l'aide de différents paradigmes : aléatoire (selon une loi de probabilité donnée), non-déterministe, ou bien décidée par un utilisateur vil et puissant.

Pour étudier le fonctionnement d'une imprimante, on représente ses exécutions par des chemins sur un graphe, dont les sommets sont les états de l'imprimante (par exemple, impression, attente, choix du document à imprimer) et les arcs sont les transitions possibles entre différents états.

Je prends le point de vue de l'utilisateur d'une imprimante, dont le pieux souhait n'est autre que de voir son document imprimé, et si possible au plus vite. Il se retrouve opposé aux autres agents (utilisateurs, non-déterminisme), et cherche à atteindre son objectif quelque soit leurs choix. Transposé dans le cadre des jeux, cette situation est interprétée par un jeu à deux joueurs : le premier joueur, Eve, représente l'utilisateur, et le second joueur, Adam, représente les agents hostiles. La condition gagnante d'Eve représente l'objectif de l'utilisateur (à savoir imprimer son document) et est opposée à celle d'Adam.

Les jeux sur les graphes permettent de décrire les propriétés que peut assurer un utilisateur qui intervient dans l'évolution d'un système ouvert.

Dans cette présentation informelle, j'expliquerai quelles sont les problèmes naturels qui apparaissent, quelles sont les méthodes utilisées pour les résoudre, et quels sont les conséquences et applications de ce modèle des jeux sur les graphes.