The Krivine machine is an abstract machine implementing the linear head reduction of λ-calculus. Ehrhard and Regnier gave a resource sensitive version returning the annotated form of a λ-term accounting for the resources used by the linear head reduction. These annotations take the form of terms in the resource calculus.

We generalize this resource-driven Krivine machine to the case of the algebraic λ-calculus. The latter is an extension of the pure λ-calculus allowing for the linear combination of λ-terms with coefficients taken from a semiring. Our machine associates a λ-term M and a resource annotation tt with a scalar α in the semiring describing some quantitative properties of the linear head reduction of M.

In the particular case of non-negative real numbers and of algebraic terms M representing probability distributions, the coefficient α gives the probability that the linear head reduction actually uses exactly the resources annotated by t. In the general case, we prove that the coefficient α can be recovered from the coefficient of tt in the Taylor expansion of M and from the normal form of tt.

La théorie des types homotopique (HoTT) est un champ de recherche ayant vu le jour dans les années 2000, qui allie une intuition topologique à l'étude des théories des types intensionnelles. L'IAS a consacré une année spéciale à l'étude de HoTT en 2012/13, culminant par la production de la référence standard, le HoTT Book. Depuis, l'intérêt envers ce nouveau sujet n'a fait que croitre.

Bien de courageux mathématiciens ont voulu attaquer le HoTT Book et se sont promptement cassés les dents sur les premiers chapitres. Cette présentation a pour but de donner une vue d'ensemble sur la théorie des types (TT), en mettant particulièrement l'emphase sur le parallèle avec la théorie de l'homotopie (Ho), dont nous présenterons aussi les notions nécessaires. Nous espérons ainsi donner assez d'intuition pour faciliter une lecture subséquente sur le sujet.

En particulier, nous expliciterons le lien entre les notions de fibration et d'espace de chemins en Ho et ceux de type dépendant et de type identité en TT, respectivement. Ceci nous permettra de voir l'axiome d'univalence de Voevodsky, un des obstacles les plus courants à la compréhension, sous un angle plus naturel.

The talk should be very introductory (so I hope) and mostly not need any in-depth knowledge of lambda-calculus and intersection type theory. It will be divided in 3 parts:

* Part 1: a crash-presentation of lambda-calculus, normalizability, the use and the scope of intersection type assignment systems, their dynamical features...

* Part 2: a presentation of de Carvalho's type system and normalizability argument: if you know a little about multisets and/or regular intersection type systems, I hope this part will be useful to you. Content : non-idempotent intersections, de Carvalho's system M_0 and a proof of the equivalence "t in typable in M_0 iff it is head-normalizing". The originality of de Carvalho's work is that, in order to prove "Typable => Normalizable", he does not resort to Tait's realizability (which is quite complicated), but to a trivial arithmetical argument. We will explain how it works.

* Part 3: If there is still enough time, I will speak of the work below. There will not be any infinitary terms or coinduction in part 1 and 2. Characterizing Weak-Normalization in an Infinitary Calculus : a Quantitative Approach.

My type is bigger than yours. And, I am sorry to say, it is also broader. The reason is: we use a coinductive type assignement system S to provide a characterization of the set of weakly normalizing (WN) terms inside an infinitary calculus called Lambda^{001}. A term is WN (w.r.t. Lambda^{001}) if it can be reduced to a normal form (NF) through at least one *sound* reduction sequence of possibly infinite length. Our work provides a new answer to Klop's problem, i.e. characterizing the finite terms whose Böhm tree does not hold bottom. Following de Carvalho's seminal work, our type system S features non-idempotent intersections. However, if de Carvalho resorted to multisets of types in order to represent intersection, we use families of types indexed by integers. The need for rigidity is motivated by the following: the infinitary, coinductive version M of de Carvalho's type system M_0, yields irrelevant derivations (the non head-normalizing term Delta Delta can be typed) and we resort to a validity criterion (called approximability) to discard them. As we will see, approximability cannot be properly defined in system M, due to an inherent non-determinism in multiset constructions.

Mon exposé commencera par une introduction sur les cartes planaires. Je présenterai ensuite les méthodes et les résultats obtenus en 2015 dans mon travail en commun avec Dominique Poulalhon et Gilles Schaeffer, en parlant d'abord du contenu d'un article de David Eppstein et Elena Mumford sur les polyèdres en coin. Notre travail consiste à compter les graphes de polyèdres en coin en déterminant la série génératrice des triangulations en coin enracinées selon leur nombre de sommets : nous en obtenons une expression explicite en fonction de la série génératrice des nombres de Catalan. Pour expliquer l'apparition des nombres de Catalan, nous donnons une décomposition algébrique directe des triangulations en coin : en particulier nous mettons en évidence une famille de triangulations en amande qui admet une décomposition structurellement équivalente à celle des arbres binaires. Pour finir nous présentons rapidement une bijection directe entre les arbres binaires et ces triangulations en amande.

Part 1 : Cette présentation a pour but d'introduire le concept d'algorithme de graphe distribué, et de donner quelques intuitions sur le sujet. En algorithmique des graphes classique, un algorithme prend un graphe en entrée et accomplit une tâche, par exemple colorer les nœuds d'une certaine manière. La version distribuée consiste à voir le graphe comme un réseau de machines, et à poser la contrainte que chaque machine ne connait qu'une petite partie du réseau : son voisinage. La question est alors de savoir quels sont les problèmes algorithmiques que l'on peut résoudre. Par exemple : est-ce que chaque sommet, en ne voyant que ses voisins dans le graphe peut choisir une couleur, telle que le résultat global est une bonne coloration du graphe ?

Il s'agira d'un exposé généraliste ne demandant pas de connaissances autre que de l'algorithmique très basique. PS : Une précision pour ceux qui veulent essayer de répondre à la question : on suppose que les sommets sont numérotés de 1 à n dans un ordre arbitraire.

Part 2 : Evolutionary game theory originated in 1973, when John Maynard Smith and George R Price had the idea to apply game theory to the evolution of species under Darwinian competition. The theory received an immediate success among theorists of evolution as it is quite simple and its predictive power is strong. It is still a very active field of research today. I will go over the developments of the field almost chronologically, from the basic concepts to the recent trends. The talk requires only highschool-level mathematics.

The word problem can be expressed as follows: Given a finite alphabet A and a finite set of generating relations R on A* (the set of the words on A*), is there an algorithm that decides whether two words in A* are equivalent modulo the relations generated by R? In general there is not, however when (A,R) has some nice properties (for example, when it forms a convergent rewriting system), then the word problem for (A,R) is decidable.

Are all the decidable word problems presented by a convergent rewriting system? Squier showed in 1987 that it is not the case. In his proof, Squier represented a word rewriting system as a 1-dimensional structure, where points are words, and where paths are relations. Squier then added an additional 2-dimensional structure generated by 2-branchings (pairs of relations starting from the same word). His work was then extended in 2012 into the construction of an infinite-dimensional object called the polygraphic resolution of the word problem (A,R), where the n-dimensional structure is generated by n-branchings. Though the construction is explicit, it is too complicated to be applied to any non-trivial example.

In this talk, I will present why n-hypercubes are a natural setting in which to reformulate (and hopefully simplify) the construction of the polygraphic resolution, where operations on branchings translate naturally into operations on the n-hypercube.

Infinitary and circular proofs are commonly used in fixed point logics. Being natural intermediate devices between semantics and traditional finitary proof systems, they are commonly found in completeness arguments, automated deduction, verification, etc. However, their proof theory is surprisingly underdeveloped. In particular, very little is known about the computational behavior of such proofs through cut elimination.

Taking such aspects into account has unlocked rich developments at the intersection of proof theory and programming language theory. One would hope that extending this to infinitary calculi would lead, e.g., to a better understanding of recursion and corecursion in programming languages. Structural proof theory is mostly based on two fundamental properties of a proof system: cut elimination and focalization.

The first one is only known to hold for restricted (purely additive) infinitary calculi, thanks to the work of Santocanale and Fortier;
the second one has never been studied in infinitary systems.

In this work, we consider the infinitary proof system μMALL∞ for multiplicative and additive linear logic extended with least and greatest fixed points, and prove these two key results. We thus establish μMALL∞ as a satisfying computational proof system in itself, rather than just an intermediate device in the study of finitary proof systems.

La complexité algébrique est le penchant algébrique de la complexité booléenne. On s'intéresse ici au calcul (ou à la représentation) efficace de polynômes par des circuits arithmétiques.

Après une courte introduction générale, nous nous concentrerons sur le cas particulier du monde non-commutatif (i.e où les variables ne commutent pas), qui est cadre naturel pour calculer des polynômes sur des domaines non-commutatifs (matrices, quaternions, etc.).

Ici, contrairement à la version commutative, sont connus pour les ABPs (Algebraic branching programs) :
- Une caractérisation exacte de la complexité à l'aide de rang de matrices (méthode de Nisan).
- Des bornes inférieures exponentielles pour des polynômes tels que le déterminant ou permanent.
- Un algorithme polynomial pour décider si un circuit calcule le polynôme nul. (Le problème "PIT", relié de manière étroite aux bornes inférieures).

Nous présenterons les idées mises en jeu dans ces résultats ainsi que quelques extensions possibles.

Part 1 : Infinitary lambda-calculus has introduced in the 90's and provides a model for indefinitely running programs that are - in a sense to be explained - productive. Some usual notions for finite lambda-terms (you-name-it normalizabilities) can naturally be extended for those infinite terms. On the other hand, type systems give a characterization of different kinds of normalization for finite terms. Recently, quantitative type systems have proven to be very useful in that respect, simplifying the realizability argument (typable => normalizable). Thus, quantitavity seem very well-fit to study normalizability issues.

Our approach consists in adapting quantitativity into an infinitary framework, by mean of replacing the unpleasant flaccidity of multiset types by sound, rigid constructions (that turn out not to impede expressivity). It yields a characterization of weak normalizabilility for infinite terms. We will exhibit a few specifities and problems related to our work, with the help of a couple of markers and a whiteboard.

Part 2 : Les mathématiques à rebours fournissent une méthode de classification de la complexité des théorèmes de la vie de tous les jours d'un point de vue calculatoire et de la théorie de la preuve. Dans cette présentation, nous introduirons les concepts clés de ce programme.

Sturmian words play a specific role in combinatorics of words, and are also studied in relation with quasicrystals; they are very useful in digital geometry for coding discrete lines (or discrete hyperplanes, in their higher-dimensional version). Nonetheless, these words have not been yet studied in a probabilistic way.

In this talk we will introduce the recurrence function in particular. This function roughly describes, in the case of a (possible not recurrent) infinite word, the gaps between occurrences of factors (consecutive blocks of letters) within the word. We will see some classical results about it and conclude with probabilistic settings that allow us to perform a probabilistic study of this parameter. This is ongoing work with Brigitte Vallée, Valérie Berthé, Eda Cesaratto and Alfredo Viola.

Reduction operators are specific projectors of a vector space. They provide a framework to do linear rewriting. More precisely, given a fixed vector space, the set of reduction operators associated with this vector space admits a lattice structure which enables us to define a notion of confluence.

During the presentation, we will explain how this lattice structure is obtained and how we can formulate the notion of confluence. We will also link together this notion of confluence and the classical one which comes from rewriting theory. Finally, if time permits, we will speak of completion and try to explain the interest of reduction operators in this situation.

Dans l'Internet, les paquets sont routés suivant le paradigme next-hop: la décision de routage ne dépend que de la destination des paquets. Le routage sensible à la source est un routage next-hop étendu où les paquets sont routés aussi en fonction de leur adresse source. Il résout des problèmes difficiles inhérents aux réseaux connectés à plusieurs fournisseurs d'accès à internet (FAI) --- on parle de réseaux multihomés: les paquets, pour une même destination, transitent par l'un ou l'autre des fournisseurs d'accès en fonction de leur adresse source. Les hôtes, en choisissant les adresses source et destination des paquets, sélectionnent des routes potentiellement différentes. Il leur est alors possible d'utiliser plusieurs routes à la fois.

Dans cet exposé, qui se veut accessible à tous (y compris ceux qui pensent que l'Internet, c'est wikipedia [1]), nous reprenons les bases du routage dans l'Internet, la notion de réseaux multihomés, et montrons pourquoi le routage sensible à la source résout des problèmes compliqués. Nous nous intéressons ensuite aux applications multi-chemin dans ces réseaux, en parlant de MPTCP [2], qui résout la plupart des problèmes, et de notre version modifiée de mosh [3].

[1] 50% des français pensent que l'Internet, c'est wikipédia, selon un sondage réalisé sur quatre personnes. [2] http://multipath-tcp.org [3] https://github.com/boutier/mosh

In this talk, I will start by giving an introduction to the quantum model of computation and quantum proof verification systems. After that, I will present a simplification of QMA complexity class, showing that it is possible to consider only "simpler" quantum states as proofs.

We introduce a lambda-calculus-style syntax, called the mu-syntax, designed to provide a crisp formalization of a biased presentation of non-skeletal cyclic operads with no distinguished output. In addition, we also prove equivalent the "entries only" and "exchangable single output" viewpoints on cyclic operads, by introducing monoidal- like defnitions for each of them (guided by the "microcosm principle" of higher category theory).

We show that mu-syntax captures this structure by proving that it is equivalent with the (unbiased) defnition of cyclic operads as algebras for a monad over the appropriate category of Markl's trees (by setting up an intermediate formalism of trees and then utilizing the non-conuence property of the mu-syntax viewed as a rewriting system).

In addition, we also prove equivalent the "entries only" and "exchangable single output" viewpoints on cyclic operads, by introducing monoidal- like defnitions for each of them (guided by the "microcosm principle" of higher category theory).

We present a complete method for synthesizing lexicographic linear ranking functions (and thus proving termination), supported by inductive invariants, in the case where the transition relation of the program includes disjunctions and existentials (large block encoding of control flow).

Previous work would either synthesize a ranking function at every basic block head, not just loop headers, which reduces the scope of programs that may be proved to be terminating, or expand large block transitions including tests into (exponentially many) elementary transitions, prior to computing the ranking function, resulting in a very large global constraint system.

In contrast, our algorithm incrementally refines a global linear constraint system according to extremal counterexamples: only constraints that exclude spurious solutions are included. Experiments with our tool Termite show marked performance and scalability improvements compared to other systems.

In 1987 Conway presented FracTran, an elegant computational model based on integer, which he proved to be Turing-complete. The simplicity of the model contrasts with its high computational power. This curious fact is usual in Computer Science, and it raise the following question: for which computational class C of functions, is the transitive closure of a function f in C recursive?

In this presentation, I will introduce some classes of relation/function of very weak expressiveness, such as Rational, Synchronous or Recognizable classes. I will then study the orbit of relations (seen as nondeterministic functions) in each of these classes. In particular, I will informally reprove Conway's result. As a corollary, I will obtain that the transitive closure of Nondeterministic Unary Finite Automata is non-recursive, that is, it is undecidable to know whether a word v belongs to the orbit of some word w.

No background required.

Les ensembles nominaux, introduits par Andrew Pitts, forment le cadre algébrique idéal pour étudier l'assignation d'une variable dans un programme. Si leur présentation usuelle est celle d'ensembles munis d'une action d'un groupe de permutation infini, on peut également les voir comme des (pré)faisceaux sur la catégorie Inj des ensembles finis et injections entre eux. Cette présentation est particulièrement pertinente lorsqu'on adopte le point de vue des théories de Lawvere à arité.

Partant de cette observation, je présenterai comment généraliser la notion d'ensemble nominal à un cadre adapté au calcul quantique. Une conséquence notable de cette généralisation est la possibilité de définir un support quantique pour les programmes considérés : on peut ainsi détecter directement sur la trace mémoire d'un programme quantique les qbits qu'il utilise réellement.

Terms of Church's lambda-calculus can be considered equivalent along many different definitions, but context equivalence is certainly the most direct and universally accepted one. If the underlying calculus becomes probabilistic, however, equivalence is too discriminating: terms which have totally unrelated behaviours are treated the same as terms which behave very similarly.

We study the problem of evaluating the distance between affine lambda-terms. The most natural definition for it, namely a natural generalisation of context equivalence, is characterised by a notion of trace distance, an bounded from above by a coinductively defined distance based on the Kantorovich metric on distributions. A different, again fully-abstract, tuple-based notion of trace distance is able to handle nontrivial examples.

Complexity Theory is a general framework to study the hardness of some tasks. Communication problems are examples of such tasks, where players receive inputs and want to compute a function (or a relation) of these inputs by exchanging some messages. Two popular measures of complexity for such problems include communication (the minimum number of bits transmitted) and information (the minimum number of "useful" bits transmitted). A first question is: are these two quantities the same?

In the classical world, the players use bits whereas in the quantum world they are allowed to use superposition of bits (qubits). So a second question is: does quantum power provides any advantage to solve such communication problems?

The goal of this talk is to present the main concepts and some recent developments in this field.

The centralizer of a language L is defined as the largest solution C(L) of the language equation XL = LX. This means that any word u.v obtained as a concatenation of a word u of L and of a word v of C(L) must admit a factorization as a word of C(L) followed by a word of L. We can understand this property as a rewriting process on the words of C(L).

Kunc designed in 2006 a regular language L in which this rewriting process simulates the transitions of a Minsky machine. However, he could deduce from this that C(L) is not recursively enumerable...

We will sketch a variant of his proof using Turing machines, and introduce the key concept of coinduction, which solves the mystery of Kunc's result: centralizers' behaviour is dual to the one of machines.

Gröbner basis have been introduced in the sixties by Shirshov and Buchberger to compute linear basis in Lie algebras and commutative algebras, respectively. In the seventies Bergman and Bokut developped Gröbner basis for associative algebras.

In this presentation, we will focus on the assocative case. We will recall the definiton of Gröbner basis, a characterisation in terms of S-polynomials (which has to be understood as a confluence property) and an algorithm of construction, the so called Buchberger's algorithm. We will introduce a natural extension of Gröbner basis: convergent linear 2-polygraphs. Linear polygraphs enables us to use higher dimensionnal categories theory to study some homological properties of associative algebras. If time permits, we will discuss this contribution.

Dans l'étude des cartes combinatoires, les constellations possèdent une position particulière. Elles sont à la fois un modèle spécial et une généralisation des cartes biparties, et elles sont aussi reliées aux problèmes de factorisation dans le groupe symétrique. Même si les constellations sont bien comprises combinatoirement grâce aux bijections, leur équation fonctionnelle a résisté jusqu'il y a peu. En genre supérieur, elles sont beaucoup moins bien comprises. Dans cet exposé, nous verrons la mise en équation des constellations dans le cas planaire et en genre supérieur, la résolution dans le cas planaire, et la rationalité en genre supérieur pour le cas biparti.

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.

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.

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.