## Soutenances de thèses

Le calendrier des séances (format iCal).

Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien.

### Séances passées

#### Année 2021

Soutenances de thèses

Mercredi 15 décembre 2021, 14 heures, Amphithéatre Gouges 1 & Youtube

**Simon Mauras** (IRIF) *Analysis of Random Models for Stable Matchings*

Stable matchings have been an extensive research topic in computer science and economics. Results in the computer science literature include the lattice structure of the set of stable matchings, and algorithms to compute it. In the economics literature, researcher have studied the incentives of agents taking part in two-sided matching markets, both from the theoretical and empirical point of views.

A recent line of works study the properties of stable matchings, using stochastic models of two-sided matching markets where the preferences of agents are drawn at random. This thesis follows this direction of inquiry, and considers two main questions: “who can manipulate?” and “who gets what?”.

The first part, addressing the question “who can manipulate?”, contains three different results. In a first result (Chapter 4), we show that when one side of the market has strongly correlated preferences, incentives to manipulate are reduced. In a second result (Chapter 5), we show that uncorrelated preferences is a worst case situation when compared to correlated preferences. Proofs of both results are based on a randomized analysis of the algorithm which computes the incentives agents have to manipulate. In a third result (Chapter 6), we study the incomplete information game where students must apply to a limited number of schools, and thus report their preferences strategically. We prove the existence of symmetric equilibria and design algorithms to compute equilibria in various special cases.

The second part, addressing the question “who gets what?”, also contains three different results. In a first result (Chapter 7), we show that under a certain input distribution of preferences, the two variants of deferred acceptance produce the same output distribution on matchings. Proofs use the lattice structure of stable matchings, show that a fixed matching has the same probability of being the top or bottom element, and give a closed formula for the probability of two agents being matched. In a second result (Chapter 8), we consider a model where the probabilities that agents like each are quantified by a “popularity” matrix, and we give evidences that the probabilities that deferred acceptance matches agents is asymptotically given by the scaled matrix where lines/columns sum up to 1. In a third result (Chapter 9), we study the time complexity of deferred acceptance, which relates to the rank people from the proposing side give to their partner. Proofs are based on a reduction to the coupon collector's problem.

Soutenances de thèses

Mardi 14 décembre 2021, 10 heures, Zoom

**Mouhamad Al-Joubbeh** (IRIF) *Minimal Separators for graphs and Paths in digraphs*

Soutenances de thèses

Lundi 13 décembre 2021, 14 heures, Room Halle 027C & Zoom

**Pierre Ohlmann** (IRIF) *Monotonic graphs for parity and mean-payoff games*

The problems of determining the winner for these two games thus belong to NP X coNP, and have attracted considerable attention since the early nineties when parity games were shown equivalent to the model-checking problem for μ-calculus. Both games moreover find numerous practical application, most notably they provide adequate models for synthesis problems on reactive systems.

Despite decades of efforts toward polynomial time algorithms, it was only recently that a breakthrough was achieved in this direction by Calude, Jain, Khoussainov, Li and Stephan, who presented in early 2017 an algorithm running in quasipolynomial time for solving parity games. Quickly after, several different algorithms with similar runtime were discovered, and later unified by the separating approach proposed by Bojańczyk and Czerwiński, and identified as value iteration algorithms.

We introduce monotonic graphs for studying structural and algorithmic aspects of such in finite duration games. These natural objects have numerous (more or less) implicit occurrences in the literature.

We start by showing that the existence of universal well-ordered such graphs characterises (half ) positionality of arbitrary winning conditions. This yields a novel approach to establishing and combining such structural results.

We then advocate that (universal) monotonic graphs provide different handles for constructing algorithms. Finite monotonic graphs induce value iteration algorithms, which are shown to be roughly equivalent to Bojańczyk and zerwiński’s separating approach in general. This allows us to formulate lower bounds for mean-payoff games, and conclude that value iteration algorithms are inadequate to improve on the current state of the art. We also study value iteration algorithms for different well-known extensions of these games.

Monotonic graphs also give a generic formalisation for strategy improvement algorithms. More precisely, we establish that valuations induced by monotonic graphs are fit for strategy improvement if and only if they are positional for the opponent. This encompasses known strategy improvement frameworks, allows us to propose new algorithms and perhaps more importantly, introduces a new tool for their difficult study.

Surprisingly, monotonic graphs also find applications for symmetric algorithms, such as those based on attractors. For parity as well as mean-payoff games, we find that monotonic graphs allow us to shed light and improve on the recent state of the art.

Soutenances de thèses

Jeudi 25 novembre 2021, 14 heures, Amphithéâtre Charpak, Campus Pierre et Marie Curie

**Federico Centrone** (IRIF) *Practical protocols for quantum communication networks*

The first concerns an interactive proof quantum protocol showing experimental evidence of computational quantum advantage in the interactive setting for the first time. In this scenario, we have a computationally unbounded quantum prover who wants to convince an honest verifier of the existence of a certain solution to a complex mathematical problem, by sending part of the proof in the form of quantum states. Our quantum scheme lets the verifier verify the prover's assertion without actually receiving the whole solution. We prove that if the agents were not allowed to use quantum resources, the verification protocol would require an exponential time in the size of the solution, leading to a quantum advantage in computational time that we could demonstrate in our laboratory.

The second copes with an electronic-voting protocol that exploits an untrusted multipartite entangled quantum source to carry on an election without relying on election authorities, whose result is publicly verifiable without compromising the robustness of the scheme and that can be readily implemented with state-of-the-art technology for a small number of voters. Unlike previous results, our scheme does not require simultaneous broadcasting and works also in noisy scenarios, where the security is bounded by the fidelity of the quantum state being used.

Last, we simulate many modes squeezed states as continuous variables Gaussian quantum networks with complex topologies, characterizing their correlations and estimating the scaling of their cost while the networks grow using a squeezing resource theory. We prove a result that allows us to enhance the entanglement between two nodes in the network by measuring the multiple paths linking them and we employ this effect to devise an entanglement routing protocol, whose performance is particularly effective on large complex networks.

Soutenances de thèses

Vendredi 12 novembre 2021, 14 heures, Online

**Léo Stefanesco** (IRIF) *Asynchronous and Relational Soundness Theorems for Concurrent Separation Logic*

Manuscript

Soutenances de thèses

Mardi 9 novembre 2021, 17 heures, Salle 3052 & Zoom

**Victor Lanvin** (IRIF) *A Semantic Foundation for Gradual Set-theoretic Types*

Set-theoretic types are well-suited to a semantic-based approach called “semantic subtyping”, in which types are interpreted as sets of values, and subtyping is defined as set-containment between these sets. We adopt this approach throughout the entirety of this thesis. Since set-theoretic types are characterized by their semantic properties, they can be easily embedded in existing type systems. This contrasts with gradual typing, which is an intrinsically syntactic concept since it relies on the addition of a type annotation to inform the type-checker not to perform some checks. In most of the existing literature, gradual typing is added by extending the subtyping relation in a syntactic way. This makes the approach very difficult to extend and generalize as this heavily depends on the system at hand.

In this thesis, we try and reconcile the two concepts, by proposing several semantic interpretations of gradual typing. The manuscript is divided into two parts. In the first part, we propose a new approach to integrate gradual typing in an existing static type system. The originality of this approach comes from the fact that gradual typing is added in a declarative way to the system by adding a single logical rule. As such, we do not need to revisit and modify all the existing rules. We then propose, for each declarative type system, a corresponding algorithmic type system, based on constraint solving algorithms. We illustrate this approach on two different systems. The first system is a Hindley-Milner type system without subtyping. We present a gradually-typed source language, a target language featuring dynamic type checks (or “casts”), as well as a compilation algorithm from the former to the latter. We then extend this language with set-theoretic types and subtyping on gradual set-theoretic types, and repeat this presentation.

In the second part of this manuscript, we explore a different approach to reconcile set-theoretic types and gradual typing. While the first part of the thesis can be seen as a logical approach to tackle this problem, the second part sets off along a more semantic strategy. In particular, we study whether it is possible to reconcile the interpretation of types proposed by the semantic subtyping approach and the interpretation of the terms of a language. The ultimate goal being to define a denotational semantics for a gradually-typed language. We tackle this problem in several steps. First, we define a denotational semantics for a simple lambda-calculus with set-theoretic types, based directly on the semantic subtyping approach. This highlights several problems, which we explain and fix by adapting the approach we used. We then extend this by giving a formal denotational semantics for the functional core of CDuce, a language featuring set-theoretic types and several complex constructs, such as type-cases, overloaded functions, and non-determinism. Finally, we study a gradually-typed lambda-calculus, for which we present a denotational semantics. We also give a set-theoretic interpretation of gradual types, which allow us to derive some very powerful results about the representation of gradual types.

Soutenances de thèses

Vendredi 22 octobre 2021, 16 heures, 3052

**Jonas Landman** (IRIF) *Quantum Algorithms for Unsupervised Machine Learning and Neural Networks*

Soutenances de thèses

Mardi 28 septembre 2021, 15 heures, Salle 3052 & Zoom

**Chaitanya Leena Subramaniam** (IRIF) *From dependent type theory to higher algebraic structures*

The second part of this dissertation concerns accessible reflective localisations of locally presentable infinity-categories. We give a definition of “pre-modulator”, and prove a canonical correspondence between pre-modulators and accessible orthogonal factorisation systems on a locally presentable infinity-category. Moreover, we show that every such factorisation system can be generated from a pre-modulator by a transfinite iteration of a “plus-construction”. We give definitions of “modulator” and “left exact modulator”, and prove that they correspond to those factorisation systems that are modalities and left-exact modalities respectively. Finally we obtain a correspondence between left-exact localisations of infinity-topoi and left-exact modulators.

Soutenances de thèses

Lundi 27 septembre 2021, 15 heures, Online via Zoom

**Zeinab Galal** (IRIF) *Bicategorical orthogonality constructions for linear logic*

Soutenances de thèses

Mercredi 7 juillet 2021, 14 heures, Salle 3052 et Zoom

**Yassine Hamoudi** (IRIF) *Quantum Algorithms for the Monte Carlo Method*

Soutenances de thèses

Mardi 29 juin 2021, 10 heures, Amphithéâtre Alan Turing & Zoom

**Rémi Nollet** (IRIF) *A study of circular representations of infinite proofs for fixed-points logics, their5expressiveness and complexity.*

Soutenances de thèses

Mardi 11 mai 2021, 15 heures, Online

**Yixin Shen** (IRIF) *Classical and quantum cryptanalysis for Euclidean lattices and subset sum*

Soutenances de thèses

Mardi 30 mars 2021, 16 heures, Online

**Nicolas Jeannerod** (IRIF) *Verification of Shell Scripts Performing File Hierarchy Transformations*

Shell is a scripting language providing control structures around Unix utility calls. Unix utilities are objects that can perform all kind of transformation on Unix filesystems. We model Unix filesystems using feature trees and transformations of Unix filesystems using formulas in a feature tree logic named FTS. We describe these modelisations extensively and discuss their validity. The control structures of Shell scripts are converted to control structures in an intermediary language that has clearly defined semantics. This involves the definition of this intermediary language, the design of a static parser for Shell scripts and of a conversion that respects the semantics of both languages. The semantics of Shell scripts is then computed using symbolic execution of the aforementioned intermediary language, using a database of specifications of Unix utility calls as formulas of FTS. The result is, for each potential trace of execution of a Shell script, a formula of FTS describing the filesystem transformation this trace performs.

The main part of the thesis then focuses on decidability of formulas of FTS. The goal is to be able to detect traces of execution of Shell scripts that cannot happen and to check properties on the Shell scripts, such as “if the script fails, then it must not have performed any transformation”. A first, theoretical, part aims at showing that the full first-order theory of FTS is decidable. This goes by first reasoning only on Σ₁-formulas of FTS and defining a system of rules R₁ that transforms Σ₁-formulas. We show that we can use R₁ to decide the satisfiability of Σ₁-formulas as well as some other properties. We then extend the reasoning from Σ₁-formulas to first-order formulas of FTS using properties of R₁ and weak quantifier eliminations. We conclude by stating that the first-order theory of FTS is indeed decidable. A second, more practical, part aims at designing efficient decision procedures for a subset of FTS rich enough to express the semantics of Unix utilities and Shell scripts. This goes by focusing on conjunctive formulas and improving on R₁. This results in a system R₂ which is more efficient on conjunctive formulas but would not have the required properties to prove decidability of the first-order. We then show how R₂ can be implemented efficiently and that it can be extended without loss of efficiency to support specific forms of Σ₁-formulas.

Finally, this thesis describes the applications of the theoretical work to the implementation of a toolchain able to analyse all software packages in the Debian distribution and report on them. We describe our analysis and the bugs that we have found during the whole project. This thesis takes place within the CoLiS project, ANR-15-CE25-0001, taking place from October 2015 to March 2021.

Soutenances de thèses

Mardi 30 mars 2021, 9 heures 30, Online

**Ranadeep Biswas** (IRIF) *Automated Formal Testing of Storage Systems and Applications*

Modern distributed software is centered around using large-scale storage systems for storing and retrieving data. To ensure persistence and availability of data in the presence of failures, these systems maintain data in multiple copies that are stored on different nodes in the network. Then, for performance reasons, these copies are allowed to (temporarily) diverge, an instance of the so-called weak-consistency, which makes the semantics of concurrent accesses to data quite complex.

Over the recent years, many solutions for implementing weakly-consistent storage systems have been proposed. These implementations are most often very complex and error-prone. The specific levels of weak consistency they ensure are most often described only informally, which makes it difficult to reason about them. Moreover, in many cases, there are significant discrepancies between the guarantees claimed in their documentation and the guarantees that they really provide.

The objective of this dissertation is to propose algorithmic techniques for automated testing of weakly-consistent distributed systems against formal specifications. We focus on an important class of distributed data types, called Conflict-Free Replicated Data Types (CRDTs for short), that include many variations like registers, flags, sets, arrays, etc., and on Transactional Systems (Databases), which enable computations on shared data that are isolated from other concurrent computations and resilient to failures. We introduce formal specifications for such systems and investigate the asymptotic complexity of checking whether a given execution conforms to such specifications. We also study the problem of testing applications that run on top of weakly-consistent transactional systems, introducing a mock in-memory storage system that simulates the behaviors of such systems according to their formal specifications.

Soutenances de thèses

Lundi 15 mars 2021, 14 heures 30, Online

**Sidi Mohamed Beillahi** (IRIF) *Automated Verification of Programs Running on top of Distributed Systems*

The effect of a set of database transactions executing in parallel is specified using a formalism called consistency model. For instance, serializability states that a set of transactions behave as if they were executed serially one after another even if they actually overlap in time. Although simple to understand, serializability carries a significant penalty on performance and modern databases implement weaker consistency models. In general, these weak models are more complex to reason about. In this dissertation, we investigate the problem of checking a property of applications called robustness. Given two comparable consistency models, an application is called robust if it has the same behaviors when ran on top of databases implementing these two models. This dissertation investigates the theoretical complexity of checking robustness in the context of several consistency models: causal consistency, prefix consistency, snapshot isolation, and serializability. It provides non-trivial reductions to a well-studied problem in formal verification, assertion checking, that enables the reuse of existing verification technology. Besides theoretical results, it proposes pragmatic approaches based on under/over-approximations that are evaluated on practical applications.

Applications ran on top of blockchain are deployed in the form of smart contracts that manipulate the blockchain state. Smart contracts are mainly used to govern trading in cryptoassets that are worth billions of US dollars, and bugs can lead to huge financial losses. Exacerbating the impact of these bugs is the fact that smart contracts cannot be modified once they are deployed on the blockchain. Applying techniques from formal verification to audit smart contracts can help in avoiding expensive bugs. However, since most smart contracts are not annotated with formal specifications, formal verification of functional properties is impeded. To overcome this problem, this dissertation investigates notions of refinement between smart contracts, which enable the re-use of verified contracts as specifications for other contracts, thus scaling up the overall verification effort.

Soutenances de thèses

Jeudi 28 janvier 2021, 15 heures, Online

**Léonard Guetta** (IRIF) *Homology of strict omega-categories*

Soutenances de thèses

Vendredi 8 janvier 2021, 9 heures 30, Online

**Simon Forest** (IRIF) *Computational Description of Higher Categories*

#### Année 2020

Soutenances de thèses

Vendredi 4 décembre 2020, 14 heures, Online

**Isaac Konan** (IRIF) *Rogers-Ramanujan type identities: bijective proofs and Lie-theoretic approach*

Soutenances de thèses

Jeudi 26 novembre 2020, 13 heures, Online

**Alexandre Nolin** (IRIF) *Communication complexity: large output functions, partition bounds, and quantum nonlocality*

Soutenances de thèses

Lundi 23 novembre 2020, 10 heures, Remote

**Alessandro Luongo** (IRIF) *Quantum algorithms for machine learning*

Soutenances de thèses

Mercredi 4 novembre 2020, 15 heures, Online

**Brieuc Guinard** (IRIF) *Intermittent Lévy Walks and their applications in biological searches*

Soutenances de thèses

Jeudi 15 octobre 2020, 16 heures, Online

**Cédric Ho Thanh** (IRIF) *Opetopes: Syntactic and Algebraic Aspects*

This thesis develops the theory of opetopes along three main axes. First, we give it clean and robust foundations by carefully detailing the approach of Kock et. al., based on polynomial monads and trees. Then, with the aim of computerized manipulation in mind, we introduce two syntactical approaches to opetopes and opetopic sets. In each, opetopes are represented as syntactical constructs whose well-formation conditions are enforced by corresponding sequent calculi. Lastly, we focus on the algebraic structures that can naturally be described by opetopes. So-called opetopic algebras include categories, planar operads, and Loday's combinads over planar trees. We show how classical results of Rezk, Joyal and Tierney (for ∞-categories), and Cisinski and Moerdijk (for ∞-operads) can be reformulated and generalized in the opetopic setting.

Manuscript

Soutenances de thèses

Vendredi 26 juin 2020, 14 heures, Online

**Baptiste Louf** (IRIF) *Cartes de grand genre : de la hiérarchie KP aux limites probabilistes*

Manuscrit

#### Année 2019

Soutenances de thèses

Mardi 17 décembre 2019, 10 heures, Salle 0010, Bâtiment Sophie Germain

**Mengchuan Zou** (IRIF) *Aspects of Efficiency in Selected Problems of Computation on Large Graphs*

In the first work, we consider a setting of classical centralized computing, and we consider the question of generalizing modular decompositions and designing time-efficient algorithm for this problem. Modular decomposition, and more broadly module detection, are ways to reveal and analyze modular properties in structured data. As the classical modular decomposition is well studied and have an optimal linear-time algorithm, we firstly study the generalizations of these concepts to hypergraphs and present here positive results obtained for three definitions of modular decomposition in hypergraphs from the literature. We also consider the generalization of allowing errors in classical graph modules and present negative results for two this kind of definitions.

The second work focuses on graph data query scenarios. Here the model differs from classical computing scenarios in that we are not designing algorithms to solve an original problem, but we assume that there is an oracle which provides partial information about the solution to the original problem, where oracle queries have time or resource consumption, which we model as costs, and we need to have an algorithm deciding how to efficiently query the oracle to get the exact solution to the original problem, thus here the efficiency is addressing to the query costs. We study the generalized binary search problem for which we compute an efficient query strategy to find a hidden target in graphs. We present the results of our work on approximating the optimal strategy of generalized binary search on weighted trees.

Our third work draws attention to the question of memory efficiency. The setup in which we perform our computations is distributed and memory-restricted. Specif- ically, every node stores its local data, exchanging data by message passing, and is able to proceed local computations. This is similar to the LOCAL/CONGEST model in distributed computing, but our model additionally requires that every node can only store a constant number of variables w.r.t. its degree. This model can also describe natural algorithms. We implement an existing procedure of multiplicative reweighting for approximating the maximum s–t flow problem on this model, this type of methodology may potentially provide new opportunities for the field of local or natural algorithms.

From a methodological point of view, the three types of efficiency concerns cor respond to the following types of scenarios: the first one is the most classical one – given the problem, we try to design by hand the more efficient algorithm; the second one, the efficiency is regarded as an objective function – where we model query costs as an objective function, and using approximation algorithm techniques to get a good design of efficient strategy; the third one, the efficiency is in fact posed as a constraint of memory and we design algorithm under this constraint.

Soutenances de thèses

Lundi 16 décembre 2019, 14 heures 30, Salle 2017, Bâtiment Sophie Germain

**Adrien Husson** (IRIF) *Logical foundations of a modelling assistant for molecular biology*

Manuscript

Soutenances de thèses

Jeudi 12 décembre 2019, 14 heures, Salle 2014, Bâtiment Sophie Germain

**Théo Zimmermann** (IRIF) *Challenges in the collaborative evolution of a proof language and its ecosystem*

Recent years have seen important changes in the development processes of Coq, of which I have been a witness and an actor (adoption of GitHub as a development platform, first for its pull request mechanism, then for its bug tracker, adoption of continuous integration, switch to shorter release cycles, increased involvement of external contributors in the open source development and maintenance process). The contributions of this thesis include a historical description of these changes, the refinement of existing processes, and the design of new ones, the design and implementation of new tools to help the application of these processes, and the validation of these changes through rigorous empirical evaluation.

Involving external contributors is also very useful at the level of the package ecosystem. This thesis additionally contains an analysis of package distribution methods, and a focus on the problem of the long-term maintenance of single-maintainer packages.

Manuscript

Soutenances de thèses

Lundi 9 décembre 2019, 14 heures, Salle 3052, Bâtiment Sophie Germain

**Simon Collet** (IRIF) *Algorithmic Game Theory Applied to Networks and Populations*

Besides the introduction and the conclusion, the thesis is divided into three parts. In the first part, we adopt the point of view of classical game theory. We propose a game that corresponds to a wide class of problems encountered in the theory of distributed computing. The main contributions of this part are, on the one hand, to show how to transform a purely algorithmic problem into a game, and, on the other hand, to prove the existence of satisfactory equilibria for the resulting class of games. This second point is essential, as it guarantees that game theory is adapted to the study of distributed games, despite their complexity.

The second part is dedicated to the study of a game omnipresent within biological systems, that we call dispersion game. This game models the situation in which a group of animals must share a certain amount of resources scattered among different geographical sites. The difficulty of the game comes from the fact that some sites contain more resources than others, but may also attract more players. We propose a rule for the distribution of resources which makes it possible to maximize the resources exploited by the whole group. This part of the thesis is also an opportunity to revisit the close links between the concept of ideal free distribution, very present in the theory of foraging, and the concept of evolutionarily stable strategy, a key concept of evolutionary game theory.

The third part focuses on the study of the behavior of a specific species of small bats living in Mexico, in the Sonoran Desert, and feeding at night from the nectar of the giant Saguaro cacti, a protected species. After the presentation of the experimental results obtained in the field, we propose a computer simulation of their behavior. The results of these simulations make it possible to formulate interesting hypotheses about the cerebral activities of these small mammals. We then study a theoretical model of game inspired by this real situation. The study of this abstract model allows us to distinguish the fundamental characteristics of the game, and to reinforce our approach of theorizing foraging behavior. This study also opens the way to applying this type of model to other situations, involving animal or human behavior.

Soutenances de thèses

Vendredi 6 décembre 2019, 15 heures 30, Salle 1009, Bâtiment Sophie Germain

**Jules Chouquet** (IRIF) *Une Géométrie du calcul : Réseaux de preuve, Appel-Par-Pousse-Valeur et topologie du Consensus*

On étudie d’abord le développement de Taylor des réseaux de preuve de la Logique Linéaire. On introduit des méthodes de démonstration qui utilisent la géométrie de l’élimination des coupures des réseaux multiplicatifs, et qui permettent de manipuler des sommes infinies de réseaux de façon sûre et correcte, pour en extraire des propriétés sur les réductions qui sont à l’œuvre.

Ensuite, nous introduisons un langage permettant de définir le développement de Taylor syntaxique pour l’Appel-Par-Pousse-Valeur (Call-By-Push-Value), en capturant certaines propriétés de la sémantique dénotationelle liées aux morphismes de coalgèbres.

Puis nous nous intéressons aux systèmes distribués (à mémoire
partagée, tolérants aux pannes), et au problème du Consensus. On
utilise un modèle topologique qui permet d’interpréter la
communication dans les complexes simpliciaux, et on l’adapte de façon
à transformer les résultats d’impossibilité bien connus en résultats
de borne inférieure de probabilité pour des algorithmes probabilistes.

*English version:*

This Phd thesis presents a quantitative study of various computation
models of fundamental computer science and proof theory, in two
principad directions: the first consists in the examination of
mecanismis of multilinear approximations in systems related to
λ-calculus and Linear Logic. The second consists in a study of
topological models for asynchronous distributed systems, and
probabilistic algorithms.

We first study Taylor expansion in Linear Logic proof nets. We introduce proof methods using the geometry of cut elimination in multiplicative nets, and which allow to work with infinite sums of nets in a safe and correct way, in order to extract properties about reduction.

Then, we introduce a language allowing us to define Taylor expansion for Call-By-Push-Value, while capturing some properties of the denotational semantics, related to coalgebras morphisms.

We focus then on fault tolerant-distributed systems with shared
memory, and to Consensus problem. We use a topological model which
allows to interpret communication with simplicial complexes, and we
adapt in so as to transform the well-known impossibility results in
lower bounds for probabilistic algorithms.

Manuscript: https://www.irif.fr/~chouquet/these.html

Soutenances de thèses

Mardi 3 décembre 2019, 14 heures 30, Salle 3052, Bâtiment Sophie Germain

**Clément Jacq** (IRIF) *Categorical Combinatorics for Non-Deterministic Innocent Strategies*

Our starting point in the thesis is provided by the combinatorial approach to innocent strategies developed by Harmer, Hyland and Melliès in a work published ten years ago. In this work, they elaborate a combinatorial description of the pointer structures of arena games, and establish that innocence can be recovered by taking advantage of a number of remarkable categorical properties, most notably the existence of a distributive law between the monad generating the Player views and the comonad generating the Opponent views.

In this thesis, we study in great detail the reconstruction of the innocent game model identified by Harmer, Hyland and Melliès, and extend this model in two directions. In the first direction, we explain how to see the Harmer-Hyland-Melliès game model as a specific instance of a dialogue category, a notion originally introduced by Melliès, using the underlying symmetry between Opponent and Player in categories of games and strategies.

In the second direction, we construct a 2-dimensional game semantics of non-deterministic PCF by equipping every game with a presheaf of non-deterministic strategies, instead of just a set of strategies. In order to perform this shift of dimension from sets to presheaves, we adapt very carefully the categorical constructions involved in the Harmer-Hyland-Melliès model, and construct in particular a pseudo-distributive law between the pseudo-monad generating the Player views and the pseudo-comonad generating the Opponent views in our non-determinic game model. We obtain in this way a bicategory of games, non-deterministic innocent strategies and simulations — which we then compare with alternative formulations of non-deterministic and innocent game semantics appearing in the literature.

Soutenances de thèses

Vendredi 21 juin 2019, 15 heures, Amphithéâtre Turing

**Nikola K. Blanchard** (IRIF) *Usability: low tech, high security*

Soutenances de thèses

Jeudi 20 juin 2019, 14 heures 30, Salle 0011

**Raphaëlle Crubillé** (IRIF) *Behavioural distances for higher-order probabilistic programs*

#### Année 2018

Soutenances de thèses

Vendredi 7 décembre 2018, 14 heures, Salle François Jacob, bâtiment Buffon

**Pierre Cagne** (IRIF) *Towards a homotopical algebra of dependent types*

Soutenances de thèses

Vendredi 30 novembre 2018, 14 heures 30, Salle 580F, Bâtiment Halle aux Farines

**Lucas Boczkowski** (IRIF) *Search and Broadcast in Stochastic Environments, a Biological Perspective*

The first model studied in this thesis takes its inspiration in collaborative transport of food in the P. Longicornis ant species. We find that some key aspects of the process are well described by a graph search problem with noisy advice. The advice corresponds to characteristic short scent marks laid in front of the load in order to facilitate its navigation. In this thesis, we provide detailed analysis of the model on trees, which are relevant graph structures from a computer science standpoint. In particular our model may be viewed as a noisy extension of binary search to trees. Tight results in expectation and high probability are derived with matching upper and lower bounds. Interestingly, there is a sharp phase transition phenomenon for the expected runtime, but not when the algorithms are only required to succeed with high probability.

The second model we work with was initially designed to capture information broadcast amongst desert ants. The model uses a stochastic meeting pattern and noise in the interactions, in a way that matches experimental data. Within this theoretical model, we present in this document a strong lower bound on the number of interactions required before information can be spread reliably. Experimentally, we see that the time required for the recruitment process of even few ants increases sharply with the group size, in accordance with our result. A theoretical consequence of the lower bound is a separation between the uniform noisy PUSH and PULL models of interaction. We also study a close variant of broadcast, without noise this time but under more strict convergence requirements and show that in this case, the problem can be solved efficiently, even with very limited exchange of information on each interaction.

Soutenances de thèses

Vendredi 23 novembre 2018, 14 heures, Laboratoire MAP5, 45 rue des Saint-pères, 7eme étage, salle du conseil

**Léo Planche** (IRIF) *Décomposition de graphes en plus courts chemins et en cycles de faible excentricité*

Soutenances de thèses

Vendredi 19 octobre 2018, 9 heures 30, Salle 580F (salle des thèses), Bâtiment Halle aux Farines

**Marie Kerjean** (IRIF) *Reflexive spaces of smooth functions: a logical account for linear partial differential equations*

This manuscript strengthens the link between proof-theory and functional analysis, and highlights the role of linear involutive negation in DiLL. The first part of this thesis consists in an overview of prerequisites on the notions of linearity, polarisation and differentiation in proof-theory, and gives the necessary background in the theory of locally convex topological vector spaces. The second part uses two standard topologies on the dual of a topological vector space and gives two models of DiLL: the weak topology allows only for a discrete interpretation of proofs through formal power series, while the Mackey topology on the dual allows for a smooth and polarised model of DiLL. Finally, the third part interprets proofs of DiLL by distributions. We detail a polarized model of DiLL in which negatives are Fr\'echet Nuclear spaces, and proofs are distributions with compact support. We show that solving linear partial differential equations with constant coefficients can be typed by a syntax similar to the one of DiLL, which we detail.

Soutenances de thèses

Jeudi 27 septembre 2018, 15 heures 30, Salle 470E, Bâtiment Halle aux Farines

**Pablo Rotondo** (IRIF) *Probabilistic studies in Number Theory and Word Combinatorics: instances of dynamical analysis*

Sturmian words are a fundamental family of words in Word Combinatorics. They are in a precise sense the simplest infinite words that are not eventually periodic. Sturmian words have been well studied over the years, notably by Morse and Hedlund (1940) who demonstrated that they present a notable number theoretical characterization as discrete codings of lines with irrational slope, relating them naturally to dynamical systems, in particular the Euclidean dynamical system. These words have never been studied from a probabilistic perspective. Here, we quantify the recurrence properties of a “random” Sturmian word, which are dictated by the so-called “recurrence function”; we perform a complete asymptotic probabilistic study of this function, quantifying its mean and describing its distribution under two different probabilistic models, which present different virtues: one is a naturaly choice from an algorithmic point of view (but is innovative from the point of view of dynamical analysis), while the other allows a natural quantification of the worst-case growth of the recurrence function. We discuss the relation between these two distinct models and their respective techniques, explaining also how the two seemingly different techniques employed could be linked through the use of the Mellin transform. In this dissertation we also discuss our ongoing work regarding two special families of Sturmian words: those associated with a quadratic irrational slope, and those with a rational slope (not properly Sturmian). Our work seems to show the possibility of a unified study.

The Continued Logarithm Algorithm, introduced by Gosper in Hakmem (1978) as a mutation of classical continued fractions, computes the greatest common divisor of two natural numbers by performing division-like steps involving only binary shifts and substractions. Its worst-case performance was studied recently by Shallit (2016), who showed a precise upper-bound for the number of steps and gave a family of inputs attaining this bound. In this dissertation we employ dynamical analysis to study the average running time of the algorithm, giving precise mathematical constants for the asymptotics, as well as other parameters of interest. The underlying dynamical system is akin to the Euclidean one, and was first studied by Chan (around 2005) from an ergodic, but the presence of powers of 2 in the quotients ingrains into the central parameters a dyadic flavour that cannot be grasped solely by studying this system. We thus introduce a dyadic component and deal with a two-component system. With this new mixed system at hand, we then provide a complete average-case analysis of the algorithm by Dynamical Analysis.

Soutenances de thèses

Mardi 25 septembre 2018, 14 heures, Salle 3052, Bâtiment Sophie Germain

**Yann Hamdaoui** (IRIF) *Concurrency, References and Linear Logic*

Soutenances de thèses

Jeudi 20 septembre 2018, 10 heures, 1828 (Olympe de Gouges)

**Matthieu Boutier** *Routage sensible à la source*

Pot en 3052 à Sophie Germain.

Soutenances de thèses

Mercredi 19 septembre 2018, 14 heures, Salle 3052, Bâtiment Sophie Germain

**Laurent Feuilloley** (IRIF) *Certification locale en calcul distribué : sensibilité aux erreurs, uniformité, redondance et interactivité*

Du fait de la contrainte de localité, peu de prédicats peuvent être vérifiés de cette manière. La certification locale est un moyen de contourner cette difficulté, et permet de décider tous les prédicats. C'est un mécanisme qui consiste à étiqueter les nœuds du réseau avec ce que l'on appelle des certificats, qui peuvent être vérifiés localement par un algorithme distribué. Un schéma de certification locale est correct si seuls les réseaux dans une configuration correcte peuvent être certifiés. L'idée de la certification locale est non seulement séduisante d'un point de vue théorique, comme une forme de non-déterminisme distribué, mais c'est surtout un concept très utile pour l'étude des algorithmes tolérants aux pannes, où une étape-clé consiste à vérifier l'état du réseau en se basant sur des informations stockées par les nœuds.

Cette thèse porte sur quatre aspects de la certification locale : la sensibilité aux erreurs, l'uniformité, la redondance et l'interactivité. L'étude de ces quatre sujets est motivée par une question essentielle : comment réduire les ressources nécessaires à la certification et/ou permettre une meilleure tolérance aux pannes? Pour aborder cette question, il est nécessaire de comprendre le mécanisme de certification en profondeur. Dans cette optique, dans cette thèse, nous apportons des réponses aux questions suivantes. À quel point les certificats doivent-ils être redondants, pour assurer une certification correcte? Les schémas de certification classiques sont-ils robustes à un changement de la condition de correction? Le fait d'introduire de l'interactivité dans le processus change-t-il la complexité de la certification?

Mots-clefs: Calcul distribué sur réseau, décision distribuée, certification locale, schéma d'étiquetage de preuve, tolérance aux pannes.

Soutenances de thèses

Mardi 18 septembre 2018, 14 heures, 580F (Halle aux Farines)

**Guillaume Claret** (IRIF) *Program in Coq*

First, we work on two preliminary projects helping us to understand the challenges of programming in Coq. The first project, Cybele, is a Coq plugin to write efficient proofs by reflection with effects. We compile and execute the impure effects in OCaml to generate a prophecy, a kind of certificate, and then interpret the effects in Coq using the prophecy. The second project, the compiler CoqOfOCaml, imports OCaml programs with effects into Coq, using an effect inference system.

Next, we describe different generic and composable representations of impure effects in Coq. The breakable computations combine the standard exceptions and mutable references effects, with a pause mechanism to make explicit the evaluation steps in order to represent the concurrent evaluation of two terms. By implementing the Pluto web server in Coq, we realize that the most important effects to program are the asynchronous inputs-outputs. Indeed, these effects are ubiquitous and cannot be encoded in a purely functional manner. Thus, we design the asynchronous computations as a first way to represent and compile programs with events and handlers in Coq.

Then, we study techniques to prove properties about programs with effects. We start with the verification of the blog system ChickBlog written in the language of the interactive computations. This blog runs one worker with synchronous inputs-outputs per client. We verify our blog using the method of specification by use cases. We adapt this technique to type theory by expressing a use case as a well-typed co-program over the program we verify. Thanks to this formalism, we can present a use case as a symbolic test program and symbolically debug it, step by step, using the interactive proof mode of Coq. To our knowledge, this is the first such adaptation of the use case specifications in type theory. We believe that the formal specification by use cases is one of the keys to verify effectful programs, as the method of use cases proved to be convenient to express (informal) specifications in the software industry. We extend our formalism to concurrent and potentially non-terminating programs with the language of concurrent computations. Apart from the use case method, we design a model-checker to verify the deadlock freeness of concurrent computations, by compiling the parallel composition to the non-deterministic choice operator.

Soutenances de thèses

Lundi 10 septembre 2018, 14 heures, Amphi Turing, Bâtiment Sophie Germain

**Luca Reggio** (IRIF) *Quantifiers and duality*

We contribute to the semantic understanding of quantifiers, from the viewpoint of duality theory, in three different areas of mathematics and theoretical computer science. First, in formal language theory through the syntactic approach provided by logic on words. Second, in intuitionistic propositional logic and in the study of uniform interpolation. Third, in categorical topology and categorical semantics for predicate logic.

Soutenances de thèses

Jeudi 5 juillet 2018, 14 heures 30, 580F (halle aux farines)

**Guillaume Lagarde** (IRIF) *Contributions to Arithmetic Complexity and Compression*

Soutenances de thèses

Vendredi 27 avril 2018, 14 heures, Salle 1021, Bâtiment Sophie Germain

**Alex B. Grilo** (IRIF) *Quantum proofs, the Local Hamiltonian problem and applications*

#### Année 2017

Soutenances de thèses

Mardi 12 décembre 2017, 14 heures 30, Salle 1009, Sophie Germain

**Fabian Reiter** (IRIF) *Distributed Automata and Logic*

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

Soutenances de thèses

Jeudi 7 décembre 2017, 14 heures 30, Amphi 10E, Halle aux Farines

**Pierre Vial** (IRIF) *Non-idempotent typing operators, beyond the lambda-calculus*

- 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.

Soutenances de thèses

Vendredi 1 décembre 2017, 14 heures 30, Salle des Thèses, Halle aux Farines

**Maxime Lucas** (IRIF) *Cubical categories for homotopy and rewriting*

Soutenances de thèses

Vendredi 17 novembre 2017, 15 heures 15, Salle 153, Olympe de Gouges

**Etienne Miquey** (IRIF) *Classical realizability and side-effects*

Soutenances de thèses

Mardi 14 novembre 2017, 11 heures, Salle des Thèses, Halle aux Farines

**Gabriel Radanne** (IRIF) *Tierless Web programming in ML*

Soutenances de thèses

Mardi 27 juin 2017, 10 heures, Salle 255, Olympe de Gouges

**Amina Doumane** (IRIF) *On the infinitary proof theory of logics with fixed points*

#### Année 2016

Soutenances de thèses

Vendredi 9 décembre 2016, 14 heures, 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, 14 heures, Salle 1006, Sophie Germain

**Wenjie Fang** (IRIF) *Aspects énumératifs et bijectifs des cartes combinatoires : généralisation, unification et application*

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.

Soutenances de thèses

Vendredi 8 avril 2016, 10 heures, Salle 2011, Sophie Germain

**Charles Grellois** (IRIF) *Sémantique de la logique linéaire et model-checking d'ordre supérieur*