Defences


Future defences



Past defences


Soutenances de thèses
mardi 12 décembre 2017, 14h30, Salle 1009, Sophie Germain
Fabian Reiter (IRIF) Distributed Automata and Logic

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

Soutenances de thèses
jeudi 07 décembre 2017, 14h30, Amphi 10E, Halle aux Farines
Pierre Vial (IRIF) Non-idempotent typing operators, beyond the lambda-calculus

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

Soutenances de thèses
vendredi 01 décembre 2017, 14h30, Salle des Thèses, Halle aux Farines
Maxime Lucas (IRIF) Cubical categories for homotopy and rewriting

Soutenances de thèses
vendredi 17 novembre 2017, 15h15, Salle 153, Olympe de Gouges
Etienne Miquey (IRIF) Classical realizability and side-effects

Soutenances de thèses
mardi 14 novembre 2017, 11h00, Salle des Thèses, Halle aux Farines
Gabriel Radanne (IRIF) Tierless Web programming in ML

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

Soutenances de thèses
mardi 27 juin 2017, 10h00, Salle 255, Olympe de Gouges
Amina Doumane (IRIF) On the infinitary proof theory of logics with fixed points

Soutenances de thèses
vendredi 09 décembre 2016, 14h00, Salle des Thèses, Halle aux Farines
Cyrille Chenavier (IRIF) Le treillis des opérateurs de réduction : applications aux bases de Gröbner non commutatives et en algèbre homologique

Soutenances de thèses
mardi 11 octobre 2016, 14h00, Salle 1006, Sophie Germain
Wenjie Fang (IRIF) Aspects énumératifs et bijectifs des cartes combinatoires : généralisation, unification et application

Le sujet de cette thèse est l'étude énumérative des cartes combinatoires et ses applications à l'énumération d’autres objets combinatoires.

Les cartes combinatoires sont un modèle combinatoire riche. Elles sont définies d’une manière intuitive et géométrique, mais elles sont aussi liées à des structures algébriques plus complexes. À la rencontre de différents domaines, les cartes peuvent être analysées par une grande variété de méthodes, et leur énumération peut aussi nous aider à compter d’autres objets combinatoires. Cette thèse présente un ensemble de résultats et de connexions très riches dans le domaine de l’énumération des cartes. Les résultats dans cette thèse se divise en deux grandes parties. La première partie contient mes travaux sur l'énumération des constellations, en utilisant les caractères du groupe symétrique ou bien en résolvant des équations fonctionnelles sur leur séries génératrices. La deuxième partie est sur le lien énumératif entre les cartes et d’autres objets combinatoires, par exemple les généralisations du treillis de Tamari et les graphes aléatoires qui peuvent être plongés dans une surface donnée.

https://www.irif.fr/~wfang/

Soutenances de thèses
vendredi 08 avril 2016, 10h00, Salle 2011, Sophie Germain
Charles Grellois (IRIF) Sémantique de la logique linéaire et model-checking d'ordre supérieur