Presentations of categories provide descriptions of categories by the means of generators, for objects and morphisms, and relations on morphisms. We generalize this notion, in order to consider situations where the objects are considered modulo an equivalence relation. This is done by adding equational morphisms to the generators for morphisms. We want to understand what it means for these equational morphisms to "behave like relations". When the equational morphisms form a convergent rewriting system on objects, three constructions can be used to define the category presented : localization (formally adding inverses to equational generators), quotient (turning equational generators into identities) and category of normal form (restricting objects to the normal forms wrt the equational morphisms).

We show that, under suitable assumptions on the presentation, the three constructions coincide.

Lien vers le papier: http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/docs/mimram_rta2015

The most famous result in the logical study of random structures is the zero-one law on random graphs, which states that every first-order definable property is asymptotically true on almost all graphs or on almost none.

In a first part, we will show how to prove the zero-one law and survey some classical results on the simplest model of random graphs, the Erdős-Rényi model G(n,p(n)). However, this is fairly unrealistic for most applications, as almost all natural graphs share some properties that the Erdős-Rényi model does not have. This motivated the study of more complex models, and we will concentrate in this talk on the configuration model, that generates the uniform distribution on graphs having a given degree sequence.

In the second part, we will show how this model can be modified to generate bipartite graphs that can be interpreted as hyper-multigraphs, using one distribution for the degrees of the vertices and one distribution for the sizes of the edges. This framework allows us to prove, for a natural class of degree distributions, a convergence law for the corresponding random hyper-(multi)graphs, and allows to recover classical results on random graphs as special cases. Furthermore, two random sequences are first-order contiguous (they have the same limit theory) if and only if their defining distributions have the same supports. This implies different natural orders on the uncountable set of limit theories defined by these distributions, and shows that as long as the moment of the distribution are not too big and the support is all of N, the limit theory is simply the limit theory of the simpler model G(n,1/n).

Word rewriting was introduced at the beginning of the 20th century in order to solve the word problem in monoids admitting a suitable (aka. finite and convergent) presentation. In 1987, Craig Squier extended it to higher dimensions, enabling him to calculate homotopical and homological properties of monoids admitting a convergent presentation.

Today, I'll start by recalling some classical rewriting properties. Then we'll use examples in order to present more recent results, together with some problems that are still open.

Automaton (semi)groups possess multiple interesting and sometimes unusual features. Very simple automata generate (counter-)examples to important conjectures in (semi)group theory. Project MealyM aims to apply computer science tools in order to investigate these (semi)groups. Here we will prove that a certain class of automata generates only torsion-free semigroups.

This is a joint work with Ines Klimann and Matthieu Picantin.

The most famous result in the logical study of random structures is the zero-one law on random graphs, which states that every first-order definable property is asymptotically true on almost all graphs or on almost none.

In a first part, we will show how to prove the zero-one law and survey some classical results on the simplest model of random graphs, the Erdős-Rényi model G(n,p(n)). However, this is fairly unrealistic for most applications, as almost all natural graphs share some properties that the Erdős-Rényi model does not have. This motivated the study of more complex models, and we will concentrate in this talk on the configuration model, that generates the uniform distribution on graphs having a given degree sequence.

In the second part, we will show how this model can be modified to generate bipartite graphs that can be interpreted as hyper-multigraphs, using one distribution for the degrees of the vertices and one distribution for the sizes of the edges. This framework allows us to prove, for a natural class of degree distributions, a convergence law for the corresponding random hyper-(multi)graphs, and allows to recover classical results on random graphs as special cases. Furthermore, two random sequences are first-order contiguous (they have the same limit theory) if and only if their defining distributions have the same supports. This implies different natural orders on the uncountable set of limit theories defined by these distributions, and shows that as long as the moment of the distribution are not too big and the support is all of N, the limit theory is simply the limit theory of the simpler model G(n,1/n).

My current working topic is the following: does a given type¹ have a unique² inhabitant?

¹: in some fixed type system
²: modulo some well-chosen notion of program equivalence

In this talk, I will describe a more specific aspect of this work, which shall serve as a termination argument for algorithms to answer the first question. In the context of the simply-typed lambda-calculus (propositional intuitionistic logic), I will answer the following question:

Given a fixed logic proof and typing environment, the number of possible programs that correspond to this proof depends on the number of free variables of each type in the type environment. If we are not interested in the precise number of programs but only "zero, one, or two-or-more", is it correct to approximate the number of variables at each type by "zero, one, or two-or-more"?

The answer and its justification are in fact rather simple. The only prerequisites for this talk are some familiarity with proof derivations for propositional logic (or typing rules for simply-typed lambda-calculus), and a vague idea of what lambda-terms are.

(If you can think about this second question and have an opinion about whether the answer is "yes" or "no", I'm interested in your guess. Would it work for "zero, one, two, or three-or-more"?)

L'exposé portera sur un sujet à la lisière entre combinatoire et géométrie mais je m'attacherai à ce qu'aucun pré-requis ne soit nécessaire à sa compréhension. Il portera sur l'associaèdre, qui est un polytope dont les faces encodent la combinatoire des dissections d'un polygone convexe. Une généralisation naturelle en est donnée par les graphes associaèdres qui contiennent également d'autres polytopes classiques, à savoir les cycloèdres et les permutaèdres. Une autre généralisation de l'associaèdre, en lien avec les algèbres amassées, est due à F.Chapoton, S.Fomin et A.Zelevinsky. Leur construction a été revisitée et généralisée par F.Santos dans le cas du type A (associaèdre classique). Dans cet exposé, je présenterai une réalisation des graphes associaèdres en tant qu'éventails simpliciaux complets avec une méthode contenant celles mentionnées précédemment dans le cas des types A et B,C.

Pendant sémantique de la correspondance preuves/programmes, la réalisabilité permet de donner des interprétations calculatoires de théories comme l'arithmétique intuitionniste. Elle est devenue "classique" grâce à des développements de Jean-Louis Krivine qui ont suivi la découverte majeure de Tim Griffin en 1990: comme des opérateurs de contrôle tels que call/cc peuvent interpréter des principes de la logique classique, on peut étendre la notion de constructivisme et la réalisabilité à des théories classiques, comme l'arithmétique de Peano au second ordre, ou même ZF, y compris avec des formes faibles de l'axiome du choix (ZF+DC (choix dépendant), qui est la théorie de base utilisée en analyse mathématique usuelle). La réalisabilité classique trouve des applications autant en informatique qu'en logique:

1) Si l'on se place du côté informatique, la motivation première de Krivine est le "problème de la spécification": pour chaque théorème mathématique, on cherche à obtenir une spécification, i.e. le comportement commun des programmes associés aux démonstrations du théorème. Par exemple, les programmes réalisant l'axiome de fondation de ZF se comportent comme un opérateur de point fixe.

2) De plus, et de façon assez inattendue, la réalisabilité classique a donné naissance à une méthode pour construire des modèles de ZF, qui généralise celles connues jusqu'ici (forcing de Cohen), et qui peut être appliquée pour prouver de nouveaux résultats de cohérence relative, par exemple que la théorie ZF+DC n'est pas suffisante pour empêcher des propriétés extrêmement pathologiques sur l'ensemble des réels. Un cas particulier des modèles de réalisabilité peut être obtenu à partir des modèles dénotationnels du lambda-calcul: cela est très intéressant car on s'aperçoit que les propriétés des modèles dénotationnels se traduisent en propriétés des modèles de ZF (par exemple, si on n'a pas le ou-parallèle, on obtient un modèle qui ne peut être obtenu par forcing).

In the last decade parallel and distributed programming has become a really important in computer science. This has brought new and exciting challenges and problems that we are just beginning to comprehend. For many years one of the problems that has plagued distributed computing research, is the lack of a core abstraction and mathematical structure to represent all the possible protocols, algorithms, tasks, etc. This structure came from a most unlikely place, combinatorial topology. A very overlooked tiny part of mathematical topology. The best part of this is that you don't need to be a topology expert to understand distributed computing.

The braid group is a generalization of the symmetric group that comes with various combinatorial and geometric interpretations. Using both these points of views, I will present some properties of the braid group, then focus on particular braids, which we call "positive braids", and on a tiny fraction of those positive braids, the so-called "simple braids".This will allow me to introduce the Garside Normal Form, which plays a key role in the combinatorics of braids and was the ground example that led to the notion of automatic normal forms and automatic groups.

In a second part of the talk, we will focus on some random walks in the semi-group of positive braids, and study the problem of the convergence of this walk, as well as some properties of the limit object we may obtain.

En vérification, une approche usuelle est le model-checking : on spécifie une propriété dans une logique, on modélise un programme dans un formalisme adapté, puis on les fait interagir afin d'établir si le programme satisfait la propriété escomptée. Avec le développement des langages fonctionnels se pose la question de vérifier des programmes d'ordre supérieur, c'est-à-dire dans lesquels une fonction peut prendre en argument des fonctions.

Nous introduirons pour modéliser ces programmes les schémas de récursion d'ordre supérieur, une sorte de système de réécriture générant l'arbre de leurs comportements. Les propriétés seront spécifiées dans une logique équivalente à un modèle d'automates d'arbres un peu particulier, les automates alternants. Un tel automate aura une exécution réussie sur l'arbre des comportements généré par un schéma de récursion d'ordre supérieur si et seulement si le programme d'origine satisfait la propriété désirée.

Une difficulté vient de la nature de ces arbres de comportement, qui n'ont pas de bonne structure de représentation (nous verrons notamment qu'ils ne sont pas réguliers en général) --- si ce n'est celle donnée par le schéma qui les engendre. L'idée fondatrice des travaux d'Ong a donc été d'incorporer dans ce modèle fini l'action de l'automate, ce qui a donné naissance à son théorème de décidabilité. Nous verrons qu'une façon alternative de procéder consiste à typer les termes correspondant au schéma avec les états de l'automate, selon une idée de Kobayashi et Ong dont je présenterai la version revisitée que Paul-André Melliès et moi avons proposée.

On s'intéresse à différentes extensions des chaînes de Markov de jonglage introduites par Warrington. Ainsi, on généralise la construction au cas du jonglage à des hauteurs arbitraires ou avec un nombre infini de balles. Dans chacun des cas, on donne des formules produits explicites pour les probabilités stationnaires et des expressions concises pour les facteurs de normalisation. On s'intéresse également à des chaînes de Markov enrichies sur des partitions d'ensembles. Enfin, on montre que dans l'un des cas étudiés, l'état stationnaire est atteint en temps fini.

Many safety and security policies can be expressed in terms of metadata that is monitored and propagated throughout the execution of a program, with significant examples including information-flow control and memory safety. Recent years have seen a steady increase in computing power, making it feasible to consider computer architectures where more resources are dedicated to security. In this talk, we will present a flexible hardware mechanism designed for enforcing such policies. The mechanism works by marking data with programmable tags that are managed by a software handler through a hardware cache. We will demonstrate how the mechanism can be used to enforce information-flow control (its original motivation), as well as other security policies, and discuss how formal verification can be used to obtain precise guarantees about the behavior of the system.

In 1941, Claude Shannon introduced a model for the Differential Analyzer, called the General Purpose Analog Computer (GPAC). Originally it was presented as a model based on circuits, where several units performing basic operations (e.g. sums, integration) are interconnected. However, Shannon itself realized that functions computed by a GPAC are nothing more than solutions of a special class of differential equations of the form y'=p(y) where p is a (vector of) polynomial. Analog computer have since been replaced by digital counterpart. Nevertheless, once can wonder whether the GPAC could in theory have super-Turing computable power.

A few years ago, it was shown that Turing-based paradigm and the GPAC have the same computational power. So, switching to analog computers would not enable us to solve the Halting problem, or any uncomputable exotic thing, but we can nonetheless compute everything a Turing machine does (given enough resources), and a return to analog technology would at least not mean a loss of computational power. However, this result did not shed any light on what happens at a computational complexity level: can an analog computer (GPAC) solve a problem faster (modulo polynomial reductions) than a digital computer (Turing machine)?

I will provide some elements which show that some reasonable restrictions of the GPAC are actually equivalent to P (polynomial time) and going even further, that we can show an equivalence with the polynomial of computable analysis. This gives an elegant, analog definition for polynomial time computable functions over real numbers.

Last seminar we talked about weighted automaton, I plan to start with this notion to build a natural generalization into a Turing-complete system (that will incidentally happen to be a lambda-calculus).

I will try to slowly generalize the matrix model and the possibility of calculation. Along the talk we will also see a few concept that are dear to us, namely the idea of operational and denotational models as well as the concept of monad and effect. If time permit it, I may be able to sketch the interest of the linear logic or of the categorical theory wrt this example.

A non deterministic finite automata is a computational model that accepts a language, namely it associates each word to a boolean value. In this talk, we will see a way to give in addition some quantitative information, by associating a word, no longer to a boolean value, but to a numerical value. The model we will talk about is the model of weighted automata.

I will give basic notions on this general model and focus on precise examples which are min-plus and max-plus automata. This talk will be very general, I will expose basic definitions and properties, as well as some decidability results about boundedness of functions computed by weighted automata.

I will present a compiler to translate OCaml programs to Coq.

OCaml is a functional programming language and Coq a proof language we develop at PPS. The aim is to have a tool to prove properties about OCaml programs and get a better understanding of links between proofs and programs.

Coq already includes a purely functional programming language thanks to the Curry-Howard correspondence. The main challenge is to handle effects (references, exceptions, non-termination, inputs/outputs), without falling into complex encodings.

Finite Automata are the weakest among the common abstract machine, which is known to characterize the class of regular languages. One can see such device as a restriction of the Turing Machine, with a single tape, scanned by a one-way read-only input head. Adding a second tape to such an automaton leads either to a transducer, if it is scanned by a one-way write-only input head, or to a two-tape automaton, otherwise.

In this talk I will focus on two-way finite state machines. The head (respectively the first head) is not restricted to one direction, but can move forward, backward or stay in place, according to the transition set.

After introducing all this terminology, I will present a construction that proves that bidirectionality does not increase the computational power of finite automata. I will then discuss the adaptation of this construction for transducers, in some restricted cases.

A graph is perfect if and only if for every induced subgraph the chromatic number is equal to the size of the maximum clique. Perfect graphs are interesting since problem like coloring, max clique or max independent set can be solve in polynomial time and also since they can arise naturally from real life problem.

In this talk I will present some well-known subclasses of perfect graph along with some of the motivations and results.

Communication Complexity is a model defined by Andrew Yao in 79 which is simple enough to be well understood. Having strong lower bounds in this model leads to lower bounds for many other models in computer science as for example streaming algorithms, data structures, property testing, VLSI, circuit complexity, decision tree, formula size…

In this talk, I will present the communication model and two very different applications: first how we can show that some language is not regular and then I will show one property testing lower bound (defining of course each of these models).

On donnera dans cet exposé une introduction à la Logique Linéaire (LL), à travers l'idée de quantification des ressources d'un programme et celle de différentiation. On commencera par introduire les espaces cohérents, le premier modèle de LL qui met en lumière un idée de linéarité. Cela nous permettra d'introduire les idées fondamentales des règles de LL. Ensuite, nous verrons comment dans les espaces de finitudes apparaissent les idées de différentiation d'une preuve, et de sémantique quantitative. Si le temps nous le permet, nous irons nous balader du coté de l'analyse fonctionnelle, et y retrouver LL.

Stone duality and its generalizations form a mathematical framework for studying the interplay between syntactic, or algebraic, and semantic, or spatio-temporal, approaches to certain areas in logic and computer science. After giving a brief introduction to this general framework, I will focus on one concrete example of an application of duality.

The application that I will discuss is part of an ongoing research project in collaboration with Bezhanishvili, Coumans and De Jongh. In this project we study fragments of intuitionistic logic and definable subsets of the universal model. I will explain all of these terms, and I will indicate how we were recently able to provide a partial solution to a classical open problem in this area, using duality theory.

I will not assume any knowledge about logic beyond classical propositional logic, nor about duality theory; the only requirement to be able to follow the talk is a basic interest in the use of mathematical methods in the study of logic.

La combinatoire analytique étudie des familles d'objets indexés par leur taille à l'aide de séries génératrices. Par exemple, pour analyser le nombre t_n d'arbres enracinés possédant n nœuds, on étudie la fonction T(z) définie par T(z) = sum t_n z^n / n!. Elle vérifie l'identité T(z) = z exp(T(z)) de laquelle on sait extraire la valeur exacte de t_n ainsi que son asymptotique. Dans cet exposé, nous verrons comment passer d'une description combinatoire des objets (les arbres enracinés) à une équation sur sa série génératrice, puis de cette équation à une valeur exacte ou asymptotique des coefficients recherchés. Les exemples comprendront toutes sortes d'arbres et de marches dans le plan ainsi que les langages algébriques non-ambiguës.

The pi-calculus is a formal language for describing independent processes that run and interact concurrently. We can also use it to explore and compare different semantics for the lambda-calculus. The encoding describes low-level mechanisms such as resource allocation, variable lookup, and flow of control, yet is flexible enough to describe call-by-value, call-by-name, or call-by-need semantics.

Le groupe de tresses à n brins est une extension naturelle du groupe symétrique à n éléments.

Je présenterai brièvement ce groupe, et en particulier une représentation graphique canonique des tresses, appelée diagrammes de courbes.

Dans un deuxième temps, je parlerai de formes normales et de propriétés désirables de ces formes normales (régularité, géodicité), qui en font un outil puissant en combinatoire énumérative et en algorithmique des groupes.

Enfin, nous observerons plus en détail une forme normale régulière, obtenue en travaillant sur les diagrammes de courbes associés aux tresses.

Pour automatiser la résolution de théorèmes, il est possible d'écrire des procédures de décision pour un domaine particulier, par exemple l'arithmétique de Presburger. Idéalement, ces procédures sont écrites et prouvées en Coq. On appelle cette technique la « preuve par réflexion ».

Je présenterai Coqbottom, notre projet en cours pour simplifier l'écriture de tels programmes. Notre méthode consiste à ajouter de manière sûre des références et exceptions au langage purement fonctionnel qu'est Coq.

http://coqbottom.gforge.inria.fr/

Je parlerai des liens entre logique, complexité de circuits booléens et théorie des automates. En effet, il est possible de caractériser les petites classes de complexité (en-dessous de NC1) à l'aide de langages réguliers. L'exemple canonique est la caractérisation d'AC° par les langages définissables dans la logique FO munie de prédicats modulaire et de l'ordre linéaire. Un résultat moins connu relie la classe linéaire AC° et la logique du premier ordre à deux variables.

Confronté à un problème pratique, la taille des fichiers objets générés par la compilation de preuves Coq, nous voulions trouver un moyen de réduire icelle.

Après un examen attentif de la situation, nous avons découvert un moyen astucieux de réduire n'importe quelle structure de données OCaml utilisée de manière purement fonctionnelle, à l'aide d'un algorithme bien connu de la théorie des automates.

Nous allons présenter cette astuce, qui est beaucoup trop simple pour ne pas mériter d'être connue !

There are two well-known algorithms for obtaining representations of integers in natural bases (binary, decimal, etc.). They are known as the "greedy algorithm" and "division algorithm". We will show how to generalise them for the complex numbers, and show that the base i-1 in the complex case plays the role of the base 2 in the real case. We will as well explain why the base i+1 is bad, it is a corollary of a very general proposition. (Based on works of Renyi, Penney and others.)

During my doctorate I'm (mainly) working on a research project called Aeolus. I will try to give you a very general view of the key ideas behind the project: what we are trying to achieve and why.

In order to get you there I will talk mostly about distributed software configuration management. I will begin with introducing some basic concepts, then I'll use a simple example of a distributed deployment (two machines: application server and database server) to illustrate these concepts and show you some interesting problems and possible solutions. After that I'll talk a little bit about certain aspects of cloud computing in context of distributed software configuration management. Finally I'll close by explaining how all that brings us to the Aeolus project.

Le modèle de streaming considère des algorithmes qui reçoivent un flux de données en entrée et disposent d'une mémoire insuffisante pour tout stocker. Il est utile à la fois pour faire des calculs en temps réel (détection de DOS, par exemple) ou pour traiter des données massives trop grosses pour la mémoire vive. Je vais présenter ce modèle puis expliquer ses liens avec la complexité de la communication. Et non, ça n'a rien à voir avec le fait de regarder des vidéos sur Youtube. Désolé.

I will present an easy introduction to game semantics. We will see the general philosophy of this model and some of its use in other domains. I will also compare the interaction of strategies in a game to the way that an operating system controls the interaction of programs with given source codes. In this sense, this semantics gives a "low level" view of the behaviors of programs, even when modeling a functional language.

Finally, I will present some elements of a syntax inspired by game semantics, which dualizes the lambda calculus. In this syntax, a new binder, lambda-bar, names the arguments passed to the environment (whereas the lambda names arguments received from the environment). This gives and alternative way to grant lambda terms the power of references.

Nous allons voir dans cet exposé quelques jeux (trop pas) rigolos, et quelques questions que les gens se posent dessus.

Jusqu’où peut-on aller dans l'abstraction d'un langage de programmation ? Peut-on laisser s’effondrer toutes les relations de complexité ? Sortir des frontières du décidable ?

Privé des arguments de complexité et de décidabilité, le scientifique informaticien est souvent sans outils. Or il y a beaucoup de choses qui y sont orthogonales ; par exemple les paradigmes (itératif, fonctionnels...).

Nous allons voir comment la thèse de Church ne nous empêche pas totalement d'avoir un œil mathématique sur cette informatique au delà de l'algorithmique.

Je parlerai de Théorie des graphes, donc on va faire des points, après on va les relier par des traits et puis on coloriera tout ça pour que ce soit plus joli.

Plus techniquement on regardera pourquoi Gyarfas a conjecturé sa fameuse conjecture (connu sous le nom de "conjecture de Gyarfas") ce qui nous amènera à découvrir la méthode dite probabiliste introduite par Paul Erdös et comment le théorème de Ramsey s'applique à quelques cas particuliers de cette conjecture.

Les entrées/sorties peuvent se faire de façon synchrone ou asynchrone. Nous sommes habitués, le plus souvent, à manipuler les E/S synchrones, comme "read" et "write" sous Unix. Celles-ci sont beaucoup plus simples à utiliser que les E/S asynchrones, qui sont pour autant la manière efficace de faire sous Windows. Ceci est particulièrement vrai dans les cas où elles sont nombreuses à devoir être faites, comme par exemple dans un serveur.

Nous verrons d'abord en détail la différence entre synchrone (bloquant), non-bloquant et asynchrone, ce qui permettra de bien comprendre chaque mécanisme, ses avantages et ses limites, puis nous décrirons les différents formalismes utilisés sous windows pour les E/S asynchrones, nous compareront leurs performances, et enfin nous parleront de l'intégration des E/S asynchrones Windows dans CPC.

Dans cet exposé j'expliquerai l'utilité du concept de «pré-ordre indexé» dans la réalisabilité et présenterai quelques exemples.

Puis, j'introduirai le concept de «pré-ordre uniforme». La catégorie des pré-ordres uniformes est une sous-catégorie de la catégorie des pré-ordres indexés qui contient la plupart des exemples provenant de la réalisabilité, et a des bonnes propriétés de fermeture.

Dans la catégorie des pré-ordres uniformes, il est possible de donner une caractérisation abstraite des «algèbres combinatoires partiels».

I will present some of the results of the Mancoosi project and introduce the assumptions and goals of the Aeolus project.

The main problem of the Mancoosi project was how to handle the complexity of assembling and managing a huge number of (packaged) components in a consistent and effective way. Effects of the work on this topic include a model of package repositories and a library of tools capable of checking various properties of a repository. Another aspect of Mancoosi was improving the upgrade experience from the point of view of the user of a repository of software packages. From this side research was focused on how to express the reconfiguration problems (Common Upgradeability Description Format was created) and how to solve them in an optimized way.

Aeolus is a project in progress, natural continuation of Mancoosi. Its goal is ”mastering cloud complexity” by creating a model of so-called cloud systems, a high level language for expressing reconfiguration requests, a low level deployment description language and preparing advanced solvers for optimized reconfiguration planning

2-player games without communication : We will adress the following 2-player problem : Alice (resp., Bob) receives a boolean x (resp., y) as input, and must return a boolean a (resp., b) as output, satisfying g(a,b) = f(x,y) for a given pair of boolean functions g and f, in absence of any communication between the two players.

We will consider different types of resources, such as randomness, quantum entanglement, and non-local boxes, and will show that for some type of games the ability for the players to use entangled quantum bits helps to produce successful outputs with higher probability than the maximum probability of success of any classical distributed protocol, and that apart from that type of games, quantum correlation does not help. The result provides an invitation to revisit the theory of distributed checking.

ReactiveML est une extension du langage OCaml avec des primitives synchrones, en particulier une notion d'instant logique global. Alors que les langages synchrones traditionnels comme Lustre ou Esterel sont utilisés pour la programmation de systèmes embarqués avec des contraintes de temps-réel, on s'intéresse ici à une programmation plus généraliste. ReactiveML est par exemple adapté pour la programmation de simulations discrète. Il a été utilisé avec succès pour l’outil GLONEMO de simulation de réseaux ad-hoc de capteurs.

Nous présenterons dans un premier temps les bases du langage et du modèle de concurrence synchrone. Nous aborderons ensuite deux travaux récents: une extension du langage appelée domaines d'horloges et une implémentation parallèle et distribuée du langage.

The number of malware is growing extraordinarily fast. Therefore, it is important to have efficient malware detectors. Malware writers try to obfuscate their code by different techniques. Many of these well-known obfuscation techniques rely on operations on the stack such as inserting dead code by adding useless push and pop instructions, or hiding calls to the operating system, etc. Thus, it is important for malware detectors to be able to deal with the program's stack. In this talk we propose a new model-checking approach for malware detection that takes into account the behavior of the stack.

Our approach consists in :(1) Modeling the program using a Pushdown System (PDS). This allows to take into account the behavior of the stack. (2) Introducing a new logic, called SCTPL, to represent the malicious behavior. SCTPL can be seen as an extension of the branching-time temporal logic CTL with variables, quantifiers, and predicates over the stack. (3) Reducing the malware detection problem to the model-checking problem of PDSs against SCTPL formulas.

We show how our new logic can be used to precisely express malicious behaviors that could not be specified by existing specification formalisms. We then consider the model-checking problem of PDSs against SCTPL specifications. We reduce this problem to emptiness checking in Symbolic Alternating Büchi Pushdown Systems, and we provide an algorithm to solve this problem. We implemented our techniques in a tool, and we applied it to detect several viruses. Our results are encouraging. This is a joint work with Tayssir Touili.

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.