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 2022

Soutenances de thèses
Vendredi 10 juin 2022, 12 heures, Online, zoom
Yiting Jiang (IRIF and ZJNU-China) Many aspects of graph coloring

Soutenances de thèses
Mardi 24 mai 2022, 14 heures, Salle 3052 & Zoom
Zhouningxin Wang (IRIF) Circular coloring, circular flow, and homomorphism of signed graphs

A signed graph is a graph $G$ together with an assignment $\sigma: \{+, -\}\to E(G)$. Graph coloring and homomorphism are two of the central problems in graph theory, and those notions and problems can be naturally extended to signed graphs. In this thesis, we introduce two dual notions: circular coloring of signed graphs and circular flow in mono-directed signed graphs, and explore the corresponding parameters: circular chromatic number and circular flow index on some classes of signed graphs. The study fits well into the framework of Jaeger's circular $\frac{2k+1}{k}$-flow problem and its dual Jaeger-Zhang conjecture on mapping planar graphs of large girth to odd cycles, and moreover, fills the parity gap by introducing the bipartite analogues of those conjectures.

In the first part of the thesis, we extend the notion of the circular coloring of graphs to signed graphs, as a refinement of Zaslavsky's $2k$-coloring of signed graphs. We develop some tools, for example, signed circular cliques, signed bipartite circular cliques and signed indicators, to determine the circular chromatic number of signed graphs. We provide bounds on the circular chromatic number of several important classes of signed graphs: signed $d$-degenerate simple graphs, signed bipartite planar simple graphs, signed planar simple graphs, and signed simple graphs whose underlying graph is $k$-colorable with arbitrary large girth.

In the second part, as a dual notion of the circular coloring of signed graphs, we introduce the notion of circular flow in mono-directed signed graphs. This is different from the widely-studied concept of the flows on bidirected signed graphs. We adapt and extend the ideas from the theory of flows on graphs to signed graphs. We provide a series of flow index results of signed graphs with given edge-connectivity conditions. Especially, the condition of $(6p-2)$-edge-connectivity is proved to be sufficient for a signed Eulerian graph to admit a circular $\frac{4p}{2p-1}$-flow. When restricted to planar graphs, we prove a stronger result that every signed bipartite planar graph of negative-girth at least $6p-2$ is circular $\frac{4p}{2p-1}$-colorable. This is so far the best negative-girth bound of the bipartite analogue of the Jaeger-Zhang conjecture.

The focus of the third part is on the homomorphism problem of signed (bipartite) planar graphs. We first provide an improved and also tight upper bound on the circular chromatic number of signed bipartite planar simple graphs using the number of vertices as a parameter. Secondly, motivated by a reformulation of the $4$-color theorem, with the newly-developed potential method, we bound from below the edge-density of $C_{-4}$-critical signed graphs and consequently, we prove that every signed bipartite planar graph of negative-girth at least $8$ maps to $C_{\Four}$ and that this girth bound is the best possible. Thirdly, using an edge-coloring result whose proof is based on the $4$-color theorem, we show that every signed bipartite planar graph of negative-girth at least $6$ admits a homomorphism to $(K_{3,3}, M)$, which could be regarded as an analogue of the Gr\“otzsch Theorem. Last, we confirm that the condition $mad(G)< \frac{14}{5}$ is sufficient for a signed graph to admit a homomorphism to $(K_6, M)$.

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

In a two sided matching market, two types of agents have preferences over one another. Examples include college admissions (students and colleges), residency programs (doctors and hospitals), job markets (workers and jobs) and, in the classical analogy, stable marriages (men and women). In a founding paper, Gale and Shapley introduced the deferred acceptance procedure, where one side proposes and the other disposes, which computes a stable matching.

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

This thesis is divided of two parts. In the first one, we study the minimal separators for graphs, and we give a new elementary proof of Menger's theorem. In the second, we study the existence of paths in chromatic-digraphs and we show that every (n+1)chromatic digraph contains a path with three blocks in which two consecutive of them are of length one. Also, we show that if the chromatic number of a digraph is greater than 4.6n, then it contains any path with three blocks of order n.

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

In a parity game, Eve and Adam take turns in moving a token along the edges of a directed graph, which are labelled by integers called priorities. This interaction results in an infinite path, and Eve wins the game if the maximal priority appearing infinitely often is even. In the more general setting of mean-payoff games, priorities are replaced by positive or negative integers interpreted as payoffs from Eve to Adam; Eve seeks to minimize their long-term average. Both parity and mean-payoff games are positional: optimal decisions can be made depending only on the current position.

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

In this thesis, we study networks of entangled quantum optical systems at different degrees of complexity, with a special regard to their application to quantum communication scenarios. In quantum communication, we want to allow two or more distant parties to exploit the properties of quantum systems to communicate in a certain way that would be unattainable with classical technology. The archetype of quantum communication is Quantum Key Distribution (QKD), that allows two agents to share a secret random key to perform secure communications, while preventing a third malicious agent from gaining knowledge about their key. In this manuscript, however, we will explore quantum communication scenarios that go beyond standard QKD in order to test the many possibilities offered by interconnected networks of quantum devices, also known as quantum internet. Specifically, we present three different types of quantum networks, that correspond to three levels of complexity of the quantum internet. In each of these levels, we describe the communication scenario, the physical requirements necessary to build the specific architecture and a novel quantum protocol that cannot be reproduced without quantum resources. In this work, we paid particular attention to the “practicality” of the protocols, namely the fact that it should be possible to implement them in realistic conditions with current technology, at least as a proof of principle.

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

The subject of this thesis is concurrent separation logic, a program logic for concurrent shared-memory languages. The relation between the proof of a program in a separation logic and the semantics of this program is expressed by the soundness theorem of this logic. This thesis introduces two soundness theorems. The first, the asynchronous soundness theorem, expresses the absence of data race in well specified programs in the language of template games in asynchronous graphs. The second part of this thesis extends the Iris concurrent separation logic with a relational soundness theorem which allows to establish simulations between a concrete program and an abstract model expressed as a state transition system. An application of this theorem is the proof of termination of concurrent programs under the assumption of a fair scheduler.

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

In this thesis, we study the interaction between set-theoretic types and gradual typing. Set-theoretic types are types containing union, intersection, and negation connectives, which are useful to type several programming language constructs very precisely. For example, union types can be used to give a very precise type to a conditional instruction, while intersection types can encode function overloading. On the other hand, gradual typing allows a programmer to bypass the type-checker, which can be useful when prototyping.

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

In this thesis, we investigate whether quantum algorithms can be used in the field of machine learning. We will first recall the fundamentals of machine learning and quantum computing and then describe more precisely how to link them through linear algebra: we introduce quantum algorithms to efficiently solve tasks such as matrix product or distance estimation. These results are then used to develop new quantum algorithms for unsupervised machine learning, such as k-means and spectral clustering. This allows us to define many fundamental procedures, in particular in vector and graph analysis. We will also present new quantum algorithms for neural networks, or deep learning. For this, we will introduce an algorithm to perform a quantum convolution product on images, as well as a new way to perform a fast tomography on quantum states. We prove that these quantum algorithms are faster equivalent to their classical version, but exhibit random effects due to the quantum nature of the computation. Many simulations have been carried out to study these effects and measure their learning accuracy on real data. Finally, we will present a quantum orthogonal neural network circuit adapted to the currently available small and imperfect quantum computers. This allows us to perform real experiments to test our theory.

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

In the first part of this dissertation, we give a definition of “dependently typed/sorted algebraic theory”, generalising the ordinary multisorted algebraic theories of Lawvere–Bénabou. Dependently sorted algebraic theories in our sense form a strict subclass of the “generalised algebraic theories” of Cartmell. We prove a classification theorem for dependently sorted algebraic theories, and use this theorem to prove the existence of dependently sorted algebraic theories for a number of varieties of algebraic structures, such as small categories, n-categories, strict and weak omega-categories, planar coloured operads and opetopic sets. We also prove a Morita equivalence between dependently sorted algebraic theories and essentially algebraic theories, showing that every locally finitely presentable category is the category of models of some dependently sorted algebraic theory. We give a definition of strict and weak homotopical models of a dependently sorted algebraic theory, and prove a rigidification theorem in a particular case. We also study the opetopic case in detail, and prove that a number of varieties of algebraic structures such as small categories and coloured planar operads can be “typed” by the category of opetopes.

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

This thesis is concerned with the bicategorical semantics of linear logic. We are specifically interested in the categorification of the relational model of linear logic with the generalized species model introduced by Fiore, Gambino, Hyland and Winskel; and its refinements using orthogonality constructions. We first present a bicategorical generalization of the model of finiteness spaces introduced by Ehrhard. We introduce an orthogonality construction on the bicategory of profunctors based on finite presentability to obtain a new bicategory where all interactions are enforced to be finite. We then consider the categorication of the computational notion of sta- bility from stable functions to stable functors. We bring together generalized species of structures and stability by refining the species model with an or- thogonality on subgroups of endomorphisms for each object in a groupoid. We show that this orthogonality allows us to restrict the analytic functors to stable functors and prove that they form a cartesian closed bicategory. We lastly study the categorification of the qualitative Scott model of linear logic and its connection with the quantitative species model of Fiore et al. We start by showing that the bicategory of profunctors with the finite coproduct pseudo-comonad is a model of linear logic that categorifies the Scott model. We then define an orthogonality between the Scott bicategory and the species bicategory that allows us to construct a new bicategory giving us a first step towards connecting linear and non-linear substitution in this setting.

Soutenances de thèses
Mercredi 7 juillet 2021, 14 heures, Salle 3052 et Zoom
Yassine Hamoudi (IRIF) Quantum Algorithms for the Monte Carlo Method

The Monte Carlo method is a central paradigm of algorithm design that consists of using statistical analysis and random sampling to solve problems that have a probabilistic interpretation. This thesis explores the advantages offered by a quantum computer to speed up this method in three directions. First, we consider the problem of estimating average values in a time-efficient way. Secondly, we study the task of importance sampling and its applications to stochastic optimization. Finally, we examine the power of quantum algorithms that operate with limited memory.

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

Post-quantum cryptography is a branch of cryptography that aims at designing non-quantum (i.e. classical) cryptographic systems, which are protected against an adversary possessing a quantum computer. In this thesis, we focus on the study of two fundamental problems for post-quantum cryptography: the shortest vector problem (SVP) and the random subset sum problem. We propose several classical/quantum algorithms that improve the state of the art.

Soutenances de thèses
Mardi 30 mars 2021, 16 heures, Online
Nicolas Jeannerod (IRIF) Verification of Shell Scripts Performing File Hierarchy Transformations

This thesis aims at applying techniques from deductive program verification and analysis of tree transformations to the problem of analysing Shell scripts. In particular, we aim at analysing Shell scripts that are used in software installation in the Debian GNU/Linux distribution. The final goal is to build a proof-of-concept tool able to read Debian packages – the way Debian has to distribute software – and report on their quality and on the potential bugs they might have.

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

As internet grows to be cheaper and faster, distributed software systems and applications are becoming more and more ubiquitous. Today they are the backbone of a large number of online services like banking, e-commerce, social networking, etc. As the popularity of these softwares increases, it is very important that they ensure strong levels of reliability and security.

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

Over the past decades, distributed software became an integral part of our society, being used in various domains like online banking or shopping, distance learning, supply chain, and telecommuting. Developing correct and efficient distributed systems is a major and timely challenge. The objective of this dissertation is to propose algorithmic techniques for improving the reliability of such software, focusing on applications ran on top of distributed storage systems like databases and blockchain. Databases allow applications to access data concurrently from multiple sites in a network. Blockchain is a cryptographically-secure distributed ledger that allows to perform irreversible actions between different parties without a trusted authority.

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

The objective of this thesis is to compare the homology of the nerve of an ω-category, invariant coming from the homotopy theory of strict ω-categories, with its polygraphic homology, invariant coming from higher rewriting theory. More precisely, we prove that both homologies generally do not coincide and call homologically coherent the particular strict ω-categories for which polygraphic homology and homology of the nerve do coincide. The goal pursued is to find abstract and concrete criteria to detect homologically coherent ω-categories.

Soutenances de thèses
Vendredi 8 janvier 2021, 9 heures 30, Online
Simon Forest (IRIF) Computational Description of Higher Categories

Higher categories are algebraic structures consisting of cells of various dimensions equipped with notions of composition, which have found many applications in mathematics (algebraic topology in particular) and theoretical computer science. They are notably complicated structures whose manipulation is technical and error-prone. The purpose of this thesis is to introduce several computational tools for strict and semi-strict variants of higher categories that ease the study of these objects. In order to represent higher categories as finite data, so that they can be given as input to a program, we use the structure of polygraph, initially introduced by Street and Burroni for strict categories and then generalized by Batanin to any algebraic theory of higher category, which allows presenting higher categories by means of systems of generators. The first problem tackled by this thesis is then the one of the word problem on strict categories, which consists in deciding whether two formal composites of cells of strict categories represent the same cell. We give an implementable and relatively efficient solution for it by improving the decidability procedure initially given by Makkai. Then, we turn to pasting diagram formalisms for strict categories, which enable to efficiently represent cells of strict categories using set-like structures and for which a reliable implementation is desirable. We consider the three main formalisms which have been introduced until now, namely Street's parity complexes, Johnson's pasting schemes and Steiner's augmented directed complexes. Our study reveals that the axiomatics of the first two ones are defective, which motivates the introduction of a new structure, called torsion-free complexes, whose axioms have nice properties and generalize those of the three other formalisms. We also show that they are amenable to concrete computation, by providing an implementation of those. Finally, we consider the problem of coherence of presentations of algebraic structures expressed in 3-dimensional weak categories, the latter being known to be equivalent to Gray categories. Taking inspiration from a celebrated result given by Squier in the context of monoids, we adapt the classical tools from rewriting theory to the setting of Gray categories and relate the coherence of presentations of Gray categories to the confluence of the critical branchings of an associated rewriting system. From this result, we deduce a semi-automated procedure to find coherent presentations of Gray categories that we apply on several examples.

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

The topic of this thesis belongs to the theory of integer partitions, at the intersection of combinatorics and number theory. In particular, we study Rogers-Ramanujan type identities in the framework of the method of weighted words. This method revisited allows us to introduce new combinatorial objects beyond the classical notion of integer partitions: the generalized colored partitions. Using these combinatorial objects, we establish new Rogers-Ramanujan identities via two different approaches. The first approach consists of a combinatorial proof, essentially bijective, of the studied identities. This approach allowed us to establish some identities generalizing many important identities of the theory of integer partitions: Schur’s identity and Göllnitz’ identity, Glaisher’s identity generalizing Euler’s identity, the identities of Siladi´c, of Primc and of Capparelli coming from the representation theory of affine Lie algebras. The second approach uses the theory of perfect crystals, coming from the representation theory of affine Lie algebras. We view the characters of standard representations as some identities on the generalized colored partitions. In particular, this approach allows us to establish simple formulas for the characters of all the level one standard representations of type A_{n-1}^{(1)},A_{2n}^{(2)},D_{n+1}^{(2)},A_{2n-1}^{(2)},B_{n}^{(1)},D_{n}^{(1)}.

Soutenances de thèses
Jeudi 26 novembre 2020, 13 heures, Online
Alexandre Nolin (IRIF) Communication complexity: large output functions, partition bounds, and quantum nonlocality

Most classical problems of communication complexity are Boolean functions. When considering functions of larger output, the way in which the result of a computation must be made available – the output model – can greatly impact the complexity of the problem. In particular, some lower bounds may not apply to all models. In this thesis, we study some lower bounds affected by the output model, problems with large outputs, revisit several classical results in the light of these output mechanisms, and relate them to the formalism of behaviors and Bell inequalities of quantum nonlocality.

Soutenances de thèses
Lundi 23 novembre 2020, 10 heures, Remote
Alessandro Luongo (IRIF) Quantum algorithms for machine learning

Cette thèse présente de nouveaux algorithmes quantiques pour l'apprentissage automatique. L'ordinateur quantique permet un nouveau paradigme de calcul qui exploite les lois de la mécanique quantique pour offrir une accélération des calculs par rapport aux ordinateurs classiques.Dans cette thèse, je propose des algorithmes quantiques pour l'apprentissage de certains modèles d'apprentissage classique. Les nouveaux algorithmes quantiques développés ont été implémentés et simulés sur des ordinateurs classiques à base d’HPC, avec les jeux de donnés couramment utilisés pour l’apprentissage automatique classique. Je démontre ainsi que ces algorithmes ont effectivement le potentiel de concourir contre les meilleurs algorithmes classiques pour l’analyse de donnés.

Soutenances de thèses
Mercredi 4 novembre 2020, 15 heures, Online
Brieuc Guinard (IRIF) Intermittent Lévy Walks and their applications in biological searches

Throughout the last two decades, a type of trajectories has been found to be almost ubiquitous in biological searches: the Lévy Patterns. Such patterns are fractal, with searches happening in self-similar clusters. Their hallmark is that their step-lengths are distributed in a power-law with some exponent μ ∈ (1, 3). This discovery lead to two intriguing questions: first, do these patterns emerge from an internal mechanism of the searcher, or from the interaction with the environment? Second, and independently of the previous question: what do these searchers have in common? When can we expect to see a Lévy Pattern of exponent μ? And how much does the knowledge of μ inform on the biological situation? Towards answering this second question, I will present an analysis of the efficiency of Lévy Walks when detection is weak, and targets appear in various sizes. In particular, I show that the much-debated inverse-square Lévy Walk is uniquely efficient in this setting. Regarding the question of how animals can perform Lévy Patterns, it has been suggested that animals could approximate a Lévy distribution by having k different modes of movement, where k = 2, 3. I will provide tight bounds for the performances of such an algorithm, which show, in accordance with the literature, that having k = 3 modes may be sufficiently efficient in biological scenarios.

Soutenances de thèses
Jeudi 15 octobre 2020, 16 heures, Online
Cédric Ho Thanh (IRIF) Opetopes: Syntactic and Algebraic Aspects

Opetopes are shapes (akin to globules, cubes, simplices, dendrices, etc.) introduced by Baez and Dolan to describe laws and coherence cells in higher-dimensional categories. In a nutshell, they are trees of trees of trees of trees of… These shapes are attractive because of their simple nature and easy to find “in nature”, but their highly inductive definition makes them difficult to manipulate efficiently.
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

Cette thèse s’intéresse aux cartes combinatoires, qui sont définies comme des plongements de graphes sur des surfaces, ou de manière équivalente comme des recollements de polygones. Le genre g de la carte est défini comme le nombre d’anses que possède la surface sur laquelle elle est plongée. En plus d’être des objets combinatoires, les cartes peuvent être représentées comme des factorisations de permutations, ce qui en fait également des objets algébriques, qu’on peut notamment étudier grâce à la théorie des représentations du groupe symétrique. En particulier, ces propriétés algébriques des cartes font que leur série génératrice satisfait la hiérarchie KP( et sa généralisation, la hiérarchie 2-Toda). La hiérarchie KP est un ensemble infini d’équations aux dérivées partielles en une infinité de variables. Les équations aux dérivées partielles de la hiérarchie KP se traduisent ensuite en formules de récurrence qui permettent d’énumérer les cartes en tout genre. D’autre part, il est intéressant d’étudier les propriétés géométriques des cartes, et en particulier des très grandes cartes aléatoires. De nombreux travaux ont permis d’étudier les propriétés géométriques des cartes planaires, c’est à dire de genre 0. Dans cette thèse, on étudie les cartes de grand genre, c’est à dire dont le genre tend vers l’infini en même temps que la taille de la carte. Ce qui nous intéressera particulièrement est la notion de limite locale, qui décrit la loi du voisinage d’un point particulier (la racine) des grandes cartes aléatoires uniformes. La première partie de cette thèse est une introduction à toutes les notions nécessaires : les cartes, bien entendu, mais également la hiérarchie KP et les limites locales. Dans un deuxième temps, on cherchera à approfondir la relation entre cartes et hiérarchie KP, soit en expliquant des formules existantes par des constructions combinatoires, soit en découvrant de nouvelles formules. La troisième partie se concentre sur l’étude des limites locales des cartes de grand genre, en s’aidant notamment de résultats obtenus grâce à la hiérarchie KP. Enfin, on conclut par quelques problèmes ouverts.

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

This thesis presents three works on different aspects of efficiency of algorithm design for large scale graph computations.

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

This thesis addresses the issue of “Executable Knowledge Representation” in the context of molecular biology. We introduce the foundation of a logical framework, termed iota, whose aim is to facilitate knowledge collation of molecular interactions at the level of proteins and at the same time allows the modeler to compile a reasonable fragment of the logic into a finite set of executable graph rewriting rules. We define a logic FO[↓] over cell state transitions. States represent cell contents; domain elements are protein parts and relations are protein-protein bindings. The unary logical operator ↓ selects transitions where as little as possible happens. Formulas over transitions also may runs, which are finite or infinite sequences of transitions. Every transition formula is also associated to a set of rewriting rules equipped with an operational semantics. We introduce two deductive systems that act as “typing” for formulas. We show that if a formula is typable in the first system then the execution of its associated rule set produces exactly the runs denoted by the formula, and that if it is typable in the second system then its associated rule set is finite. We introduce a grammar that produces formulas typable in both systems, up to logical equivalence. Finally we study decidability and definability properties of fragments of FO[↓]. In particular, we show that formulas typable in the second system are in a tight fragment of FO, which implies that the operator ↓ can then be eliminated.

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

In this thesis, I present the application of software engineering methods and knowledge to the development, maintenance, and evolution of Coq —an interactive proof assistant based on type theory— and its package ecosystem. Coq has been developed at Inria since 1984, but has only more recently seen a surge in its user base, which leads to much stronger concerns about its maintainability, and the involvement of external contributors in the evolution of both Coq, and its ecosystem of plugins and libraries.

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

The aim of this thesis is to use algorithmic game theory tools to study various games inspired from real world problems in the fields of information networks and biology. These games are characterized by a large number of players, each with incomplete information about other players. In classical game theory, these games fall into the category of extensive games with imperfect information, which are modeled using trees. However, these games remain very difficult to analyze in details, because of their intrinsic complexity, which is linked with their possibly infinite tree depth. Nevertheless, we have taken up the challenge of this task, while diversifying the methods of resolution, and emphasizing its interdisciplinary aspect.

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

Cette thèse propose une étude quantitative de plusieurs modèles de calcul de l’informatique fondamentale et de la théorie de la démonstration. Deux approches sont menées : la première consiste à examiner les mécanismes d’approximation multilinéaires dans des systèmes issus du λ-calcul et de la Logique Linéaire. La seconde consiste à étudier les modèles topologiques pour les systèmes distribués et à les adapter aux algorithmes probabilistes.

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

Twenty-five years ago, Hyland and Ong resolved the full abstraction problem for the PCF language by constructing a game semantics based on the fundamental notion of innocent strategy. We carry on their work in this thesis, and construct a 2-dimensional category of non-deterministic and innocent strategies extending their original deterministic innocent game model.

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

The manuscript is available at: http://research.crubille.lautre.net/main.pdf

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

This thesis is built around two series of works, each motivated by experiments on ants. We derive and analyse new models that use computer science concepts and methodology, despite their biological roots and motivation.

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é

En collaboration avec des chercheurs en biologie à Jussieu, nous étudions des graphes issus de données biologiques afin de d'en améliorer la compréhension. Ces graphes sont constitués à partir de fragments d'ADN, nommés reads. Chaque read correspond à un sommet, et deux sommets sont reliés si les deux séquences d'ADN correspondantes ont un taux de similarité suffisant. Ainsi se forme des graphes ayant une structure bien particulière que nous nommons hub-laminaire. Un graphe est dit hub-laminaire s'il peut être résumé en quelques plus courts chemins dont tous les sommets du graphe soient proche. Nous étudions en détail le cas où le graphe est composé d'un unique plus court chemin d'excentricité faible. Nous améliorons la preuve d'un algorithme d'approximation déjà existant et en proposons un nouveau, effectuant une 3-approximation en temps linéaire. De plus, nous analysons le lien avec le problème de k-laminarité défini par Michel Habib et Finn Völkel, ce dernier consistant en la recherche d'un diamètre de faible excentricité. Nous étudions ensuite le problème du cycle isométrique de plus faible excentricité. Nous montrons que ce problème est NP-complet et proposons deux algorithmes d'approximations. Nous définissons ensuite précisément la structure “hub-laminaire” et présentons un algorithme d'approximation en temps O(nm). Nous confrontons cet algorithme à des graphes générés par une procédure aléatoire et l'appliquons à nos données biologiques. Pour finir nous montrons que le calcul du cycle isométrique d'excentricité minimale permet le plongement d'un graphe dans un cercle avec une distorsion multiplicative faible. Le calcul d'une décomposition hub-laminaire permet quant à lui une représentation compacte des distances avec une distorsion additive bornée.

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

Around the Curry-Howard correspondence, proof-theory has grown along two distinct fields: the theory of programming languages, for which formulas acts as data types, and the semantic study of proofs. The latter consists in giving mathematical models of proofs and programs. In particular, denotational semantics distinguishes data types which serves as input or output of programs, and allows in return for a finer understanding of proofs and programs. Linear Logic (LL) gives a logical interpretation of the basic notions of linear algebra, while Differential Linear Logic allows for a logical understanding of differentiation.

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

Dynamical Analysis incorporates tools from dynamical systems, namely the Transfer Operator, into the framework of Analytic Combinatorics, permitting the analysis of numerous algorithms and objects naturally associated with an underlying dynamical system. This dissertation presents, in the integrated framework of Dynamical Analysis, the probabilistic analysis of seemingly distinct problems in a unified way: the probabilistic study of the recurrence function of Sturmian words, and the probabilistic study of the Continued Logarithm algorithm.

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

The topic of this thesis is the study of the encoding of references and concurrency in Linear Logic. Our perspective is to demonstrate the capability of Linear Logic to encode side-effects to make it a viable, formalized and well studied compilation target for functional languages in the future. The key notion we develop is that of routing areas: a family of proof nets which correspond to a fragment of differential linear logic and which implements communication primitives. We develop routing areas as a parametrizable device and study their theory. We then illustrate their expressivity by translating a concurrent λ-calculus featuring concurrency, references and replication to a fragment of differential nets. To this purpose, we introduce a language akin to Amadio’s concurrent λ-calculus, but with explicit substitutions for both variables and references. We endow this language with a type and effect system and we prove termination of well-typed terms by a mix of reducibility and a new interactive technique. This intermediate language allows us to prove a simulation and an adequacy theorem for the translation.

Soutenances de thèses
Jeudi 20 septembre 2018, 10 heures, 1828 (Olympe de Gouges)
Matthieu Boutier Routage sensible à la source

En routage next-hop, paradigme de routage utilisé dans l'Internet Global, chaque routeur choisit le next-hop de chaque paquet en fonction de son adresse destination. Le routage sensible à la source est une extension compatible du routage next-hop où le choix du next-hop dépend de l'adresse source du paquet en plus de son adresse destination. Nous montrons dans cette thèse que le routage sensible à la source est adapté au routage des réseaux multihomés avec plusieurs adresses, qu'il est possible d'étendre de manière compatible les protocoles de routage à vecteur de distance existants et que ce paradigme de routage offre avantageusement plus de flexibilité aux hôtes. Nous montrons d'abord que certains systèmes n'ordonnent pas correctement les entrées sensibles à la source dans leurs tables de routage et nous définissons un algorithme adapté aux protocoles de routage pour y remédier. Nous montrons comment étendre les protocoles à vecteur de distances au routage sensible à la source de manière compatible. Nous validons notre approche en concevant une extension d'un protocole existant (Babel), en réalisant la première implémentation complète d'un protocole sensible à la source et en utilisant ce protocole pour router un réseau multihomé. Enfin, nous montrons que le routage sensible à la source offre des possibilités de multichemin aux couches supérieures des hôtes. Nous vérifions qu'il s'intègre aux technologies existantes (MPTCP) et nous concevons des techniques d'optimisation pour les applications légères. Nous évaluons ces techniques après les avoir implémentées dans le cadre d'une application existante (mosh).

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é

Cette thèse porte sur la notion de certification locale, un sujet central en décision distribuée, un domaine du calcul distribué. Le mécanisme de la décision distribuée consiste, pour les nœuds d'un réseau, à décider de manière distribuée si le réseau est dans une configuration correcte ou non, selon un certain prédicat. Cette décision est dite locale, car les nœuds du réseau ne peuvent communiquer qu'avec leurs voisins. Après avoir communiqué, chaque nœud prend une décision, exprimant si le réseau est correct ou non localement, c'est-à-dire correct étant donné l'information partielle récoltée jusque-là. Le réseau est déclaré correct globalement s'il est déclaré correct localement par tous les nœuds.

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

In this thesis, we develop new techniques to conveniently write formally verified programs. To proceed, we study the use of Coq as a programming language in different settings. Coq being a purely functional language, we mainly focus on the representation and on the specification of impure effects, like exceptions, mutable references, inputs-outputs, and concurrency.

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

The unifying theme of the thesis is the semantic meaning of logical quantifiers. In their basic form quantifiers allow to state the existence, or non-existence, of individuals satisfying a property. As such, they encode the richness and the complexity of predicate logic, as opposed to propositional logic.

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

This thesis explores two territories of computer science: complexity and compression. More precisely, in a first part, we investigate the power of non-commutative arithmetic circuits, which compute multivariate non-commutative polynomials. For that, we in- troduce various models of computation that are restricted in the way they are allowed to compute monomials. These models generalize previous ones that have been widely studied, such as algebraic branching programs. The results are of three different types. First, we give strong lower bounds on the number of arithmetic operations needed to compute some polynomials such as the determinant or the permanent. Second, we design some deterministic polynomial-time algorithm to solve the white-box polynomial identity testing problem. Third, we exhibit a link between automata theory and non-commutative arithmetic circuits that allows us to derive some old and new tight lower bounds for some classes of non-commutative circuits, using a measure based on the rank of a so-called Hankel matrix. A second part is concerned with the analysis of the data compression algorithm called Lempel-Ziv. Although this algorithm is widely used in practice, we know little about its stability. Our main result is to show that an infinite word compressible by LZ’78 can become incompressible by adding a single bit in front of it, thus closing a question proposed by Jack Lutz in the late 90s under the name “one-bit catastrophe”. We also give tight bounds on the maximal possible variation between the compression ratio of a finite word and its perturbation—when one bit is added in front of it.

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

Manuscript is available here: https://www.irif.fr/~abgrilo/thesis.pdf

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

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 7 décembre 2017, 14 heures 30, 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.

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

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.

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

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.

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