Developing a descriptive complexity theory for distributed computing; that was the major motivation for my PhD thesis. To clarify what this means, I will first illustrate the principle of descriptive complexity using Fagin’s theorem, and then explain how that principle can be adapted to the setting of distributed computing. After that, I will present the two main contributions of my thesis: a class of distributed automata that is equivalent to monadic second-order logic on graphs, and another class that is equivalent to a small fragment of least fixpoint logic (more specifically, to a restricted variant of the modal μ-calculus that allows least fixpoints but forbids greatest fixpoints). In both cases, the considered model of distributed computing is based on finite-state machines.

Manuscript: https://www.irif.fr/~reiterf

L'objet de cette thèse est l'extension des méthodes de la théorie des types intersections non-idempotents, introduite par Gardner et de Carvalho, à des cadres dépassant le lambda-calcul stricto sensu.

• Nous proposons d'abord une caractérisation de la normalisation de tête et de la normalisation forte du lambda-mu calcul (déduction naturelle

classique) en introduisant des types unions non-idempotents. Comme dans le cas intuitionniste, la non-idempotence nous permet d'extraire du typage des informations quantitatives ainsi que des preuves de terminaison beaucoup plus élémentaires que dans le cas idempotent. Ces résultats nous conduisent à définir une variante à petits pas du lambda-mu-calcul, dans lequel la normalisation forte est aussi caractérisée avec des méthodes quantitatives.

• Dans un deuxième temps, nous étendons la caractérisation de la normalisation faible dans le lambda-calcul pur à un lambda-calcul infinitaire étroitement lié aux arbres de Böhm et dû à Klop et al. Ceci donne une réponse positive à une question connue comme le problème de Klop. À cette fin, il est nécessaire d'introduire conjointement un système (système S) de types infinis utilisant une intersection que nous qualifions de séquentielle, et un critère de validité servant à se débarrasser des preuves dégénérées auxquelles les grammaires coinductives de types donnent naissance. Ceci nous permet aussi de donner une solution au problème n°20 de TLCA (caractérisation par les types des permutations héréditaires). Il est à noter que ces deux problèmes n'ont pas de solution dans le cas fini (Tatsuta, 2007).
• Enfin, nous étudions le pouvoir expressif des grammaires coinductives de types, en dehors de tout critère de validité. Nous devons encore recourir au système S et ous montrons que tout terme est typable de façon non triviale avec des types infinis et que l'on peut extraire de ces typages des informations sémantiques comme l'ordre (arité) de n'importe quel lambda-terme. Ceci nous amène à introduire une méthode permettant de typer des termes totalement non-productifs, dits termes muets, inspirée de la logique du premier ordre. Ce résultat prouve que, dans l'extension coinductive du modèle relationnel, tout terme a une interprétation non vide. En utilisant une méthode similaire, nous montrons aussi que le système S collapse surjectivement sur l'ensemble des points de ce modèle.

https://www.irif.fr/~pvial/defense.htm

https://www.irif.fr/users/mlucas/index

https://www.irif.fr/~emiquey/these/

Eliom est un dialecte d’OCaml pour la programmation Web qui permet, à l’aide d’annotations syntaxiques, de déclarer code client et code serveur dans un même fichier. Ceci permet de construire une application complète comme un unique programme distribué dans lequel il est possible de définir des widgets aisément composables avec des comportements à la fois client et serveur. Eliom assure un bon comportement des communications grâce à un système de type et de nouvelles constructions adaptés à la programmation Web. De plus, Eliom est efficace : un découpage statique sépare les parties client et serveur durant la compilation et évite de trop nombreuses communications entre le client et le serveur. Enfin, Eliom supporte la modularité et l’encapsulation grâce à une extension du système de module d’OCaml permettant l’ajout d’annotations indiquant si une définition est présente sur le serveur, le client, ou les deux. Cette thèse présente la conception, la formalisation et l’implémention du langage Eliom.

https://www.irif.fr/~gradanne/phdthesis.html

n this thesis, we examine different frameworks for the general theory of cyclic operads of Getzler and Kapranov. As suggested by the title, we set up theoretical grounds of syntactic, algebraic and categorified nature for the notion of a cyclic operad.In the syntactic treatment, we propose a lambda-calculus-style formal language, called mu-syntax, as a lightweight representation of the entries-only cyclic operad structure. As opposed to the original exchangeable-output characterisation of cyclic operads, according to which the operations of a cyclic operad have inputs and an output that can be “exchanged” with one of the inputs, the entries-only cyclic operads have only entries (i.e. the output is put on the same level as the inputs). By employing the rewriting methods behind the formalism, we give a complete step-by-step proof of the equivalence between the unbiased and biased definitions of cyclic operads.Guided by the microcosm principle of Baez and Dolan and by the algebraic definitions of operads of Kelly and Fiore, in the algebraic approach we define cyclic operads internally to the category of Joyal’s species of structures. In this way, both the original exchangeable-output characterisation of Getzler and Kapranov, and the alternative entries-only characterisation of cyclic operads of Markl are epitomised as “monoid-like” objects in “monoidal-like” categories of species. Relying on a result of Lamarche on descent for species, we use these “monoid-like” definitions to prove the equivalence between the exchangeable-output and entries-only points of view on cyclic operads.Finally, we establish a notion of categorified cyclic operad for set-based cyclic operads with symmetries, defined in terms of generators and relations. The categorifications we introduce are obtained by replacing sets of operations of the same arity with categories, by relaxing certain defining axioms, like associativity and commutativity, to isomorphisms, while leaving the equivariance strict, and by formulating coherence conditions for these isomorphisms. The coherence theorem that we prove has the form “all diagrams of canonical isomorphisms commute”.For entries-only categorified cyclic operads, our proof is of syntactic nature and relies on the coherence of categorified operads established by Došen and Petrić. We prove the coherence of exchangeable-output categorified cyclic operads by “lifting to the categorified setting” theequivalence between entries-only and exchangeable-output cyclic operads, set up previously in the algebraic approach.

In this thesis, we study Mealy automata, i.e. complete, deterministic, letter-to-letter transducers which have same input and output alphabet. These automata have been used since the 60s to generate (semi)groups that sometimes have remarkable properties, that were used to solve several open problems in (semi)group theory. In this work, we focus more specifically on the possible contributions that theoretical computer science can bring to the study of these automaton (semi)groups.The thesis consists of two main axis. The first one, which corresponds to the Chapters II and III, deals with decision problems and more precisely with the Burnside problem in Chapter II and with singular points in Chapter III. In these two chapters, we link structural properties of the automaton with properties of the generated group or of its action. The second axis, which comprises the Chapter IV, is related with random generation of finite groups. We seek, by drawing random Mealy automata in specific classes, to generate finite groups, and obtain a convergence result for the obtained distribution. This result echoes Dixon's theorem on random permutation groups

This thesis examines some quantitative questions in the framework of two different stochastic models. It is divided into two parts: the first part examines a new class of stochastic games with priority payoff. This class of games contains as proper subclasses the parity games extensively studied in computer science, and limsup and liminf games studied in game theory. The second part of the thesis examines some natural but involved questions about distributions, studied in the simple framework of finite state Markov chain.In the first part, we examine two-player zero-sum games focusing on a particular payoff function that we call the priority payoff. This payoff function generalizes the payoff used in parity games. We consider both turn-based stochastic priority games and concurrent priority games. Our approach to priority games is based on the concept of the nearest fixed point of monotone nonexpansive mappings and extends the mu-calculus approach to priority games.The second part of the thesis deals with population questions. Roughly speaking, we examine how a probability distribution over states evolves in time. More specifically, we are interested in questions like the following one: from an initial distribution, can the population reach at some moment a distribution with a probability mass exceeding a given threshold in state Goal? It turns out that this type of questions is much more difficult to handle than the questions concerning individual trajectories: it is not known for the simple model of Markov chains whether population questions are decidable. We study restrictions of Markov chains ensuring decidability of population questions.

https://www.irif.fr/~doumane/defense.htm