Defences

The calendar of events (iCal format).
In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link.



Year 2023

PhD defences
Wednesday January 25, 2023, 1:30PM, Amphithéâtre Alan Turing & Zoom
Farzad Jafarrahmani (IRIF) Fixpints of Types in Linear Logic from a Curry-Howard-Lambek Perspective

This thesis is concerned with the studying of an extension of the propositional linear logic with fixpoints of type from a Curry-Howard-Lambek perspective. Linear logic with fixpoints of types, called MULL, allows us to have inductive and coinductive proofs. We develop a categorical semantics of MULL based on Seely categories and on strong functors acting on them. Then we introduce and study MULLP as an extension of Polarized Linear Logic, with least and greatest fixpoints. Taking advantage of the implicit structural rules of MULLP, we introduce a term syntax for this language, in the spirit of the classical λ-calculus and of system L. We equip this logical system with a deterministic reduction semantics as well as a categorical semantic. We always examine our categorical semantics with concrete cases such as category of sets and relations, category of sets equipped with a notion of totality (non-uniform totality spaces) and relations preserving, and coherence spaces with totality. In the case of MULLP, we prove an adequacy result for MULLP between its operational and denotational semantics, from which we derive a normalization property thanks to the properties of the totality interpretation. We will also study non-wellfounded proofs in linear logic, which one can see as an extension of inductive proofs, from a denotational semantics point of view by making a relation between validity condition for non-wellfounded proofs and totality interpretation. Finally, we will provide a categorical setting for the exponentials that are encoded using fixpoints operator.


Year 2022

PhD defences
Thursday December 15, 2022, 5PM, Online
Berk Cirisci (IRIF) Formal Verification of Concurrent Data Structures

Modern automated services rely on concurrent software where multiple requests are processed by different processes at the same time. These processes execute concurrently either in a single machine or in a distributed system with multiple machines built on top of a network. The requests are typically about processing data which is stored in data structures that provide implementations of common abstract data types (ADTs) such as queues, key-value stores, and sets. The data structures themselves are concurrent in the sense that they support operations that can execute concurrently at the same time. Developing such concurrent data structures or even understanding and reasoning about them can be tricky. This is coming from the fact that synchronization between operations of these data structures must be minimized to reduce response time and increase throughput, yet this minimal amount of synchronization must also be adequate to ensure conformance to their specification. These opposing statements, along with the general challenge in reasoning about interleavings between operations make concurrent data structures a ripe source of insidious programming errors that are difficult to reproduce, locate, or fix. Therefore, verification techniques that can check the correctness of a concurrent data structure or (if it is not correct) that can detect, pinpoint and fix the errors in it, are invaluable. In this thesis, we introduce new algorithmic approaches for improving the reliability of concurrent data structures. For shared-memory data structures (where processes communicate using a shared memory), we introduce new algorithms for finding safety violations (if any) and repairing the implementation in order to exclude these violations. For data structures running on top of a network, we focus on the underlying consensus protocols and provide a new proof methodology for checking their safety specification which is based on refinement.

PhD defences
Thursday December 1, 2022, 2PM, Salle 3052 du bâtiment Sophie Germain & Zoom
Abhishek De (IRIF) Linear logic with least and greatest fixed points: truth semantics, complexity, and a parallel syntax

The subject of this thesis is the proof theory of linear logic with the least and greatest fixed points. In the literature, several systems have been studied for this language viz. the wellfounded system that relies on Park's induction rule, and systems that implicitly characterise induction such as the circular system and the non-wellfounded system. This thesis contributes to the theory of these systems with the ultimate goal of exactly capturing the provability relation of these systems and application of these objects in programming languages supporting (co)inductive reasoning. This thesis contains three parts. In the first part, we recall the literature on linear logic and the main approaches to the proof theory of logics with fixed points. In the second part, we obtain truth semantics for the wellfounded system, devise new wellfounded infinitely branching systems, and compute the complexity of provability in circular and non-wellfounded systems. In the third part, we devise non-wellfounded proof-nets and study their dynamics.

Manuscript

PhD defences
Friday November 18, 2022, 1:30PM, Salle 0011 du bâtiment Sophie Germain & Zoom
Loïc Peyrot (IRIF) From Proof Terms to Programs. An operational and quantitative study of intuistionistic Curry-Howard calculi

The λ-calculus is a mathematical model of functional programming languages, with an emphasis on function application. Variants of the calculus are of interest to model specific computational behaviors.

The atomic λ-calculus and the λ-calculus with generalized applications are two (independent) variants of the λ-calculus originating in computational interpretations of proof theory. While programming languages are built from specific deterministic evaluation strategies, the existing literature on the atomic λ-calculus and generalized applications only go over the general theory of the calculi. In particular, reduction of terms is unrestricted, and only analyzed qualitatively. This induces a gap between theory and practice, which we strive to diminish in this thesis.

Starting from the atomic λ-calculus, we isolate the most salient concept of its operational semantics, that we call node replication. This is a particular substitution procedure, which duplicates terms finely, one node of the syntax tree at a time. We follow up with λ-calculi with generalized applications. They use a ternary application constructor, adding a continuation to the usual binary application. In this work, we develop the operational theories built on node replication and generalized applications separately. For the two of them: On an operational level, we give several evaluation strategies, all observationally equivalent to the corresponding strategies in the λ-calculus. On a logical level, our approach is guided by quantitative types. We provide different type systems that inductively characterize semantic properties, but also give quantitative bounds on the length of reduction and the size of normal forms.

More precisely, in the first part of this thesis, we implement node replication by means of an explicit substitution calculus. We show in particular how node replication can be used to implement full laziness, a well-known evaluation strategy for functional programming languages like Haskell. We prove observational equivalence properties relating the fully lazy semantics with the standard ones. In the second part of the thesis, we start with an operational and logical characterization of solvability in λ-calculi with generalized applications. We show how this framework gives rise to a remarkable operational theory of call-by-value. The call-by-name characterization relies on an original calculus with generalized applications. We show in both cases that the operational semantics are compatible with a quantitative model, unlike the one of the original call-by-name calculus. We then prove essential properties of this new call-by-name calculus, and show observational equivalence with the original one.

PhD defences
Thursday November 17, 2022, 10AM, 1002
Pierre Nigron Effectful programs and their proofs in type theory : application to certified packet processing

PhD defences
Monday November 7, 2022, 2PM, Université Côte d'Azur
Mehdi Zaïdi Dualité pour le fragment existentiel de la logique du premier ordre sur les mots

This thesis fits in the area of research that investigates the application of topological duality methods to problems that appear in theoretical computer science.One of the eventual goals of this approach is to derive results in computational complexity theory by studying appropriate topological objects which characterise them.The link which relates these two seemingly separated fields is logic, more precisely a subdomain of finite model theory known as logic on words. It allows for a description of complexity classes as certain families of languages, possibly non-regular, on a finite alphabet.Very little is known about the duality theory relative to fragments of first-order logic on words which lie outside of the scope of regular languages. The contribution of ourwork is a detailed study of such a fragment. Fixing an integer k ≥ 1, we consider the Boolean algebra BΣ1[Nuk ]. It corresponds to the fragment of logic on words consisting in Boolean combinations of sentences defined by using a block of at most k existential quantifiers, letter predicates and uniform numerical predicates of arity l ∈ {1, …, k}.We give a detailed study of the dual space of this Boolean algebra, for any k ≥ 1, andprovide several characterisations of its points. In the particular case where k = 1, weare able to construct a family of ultrafilter equations which characterise the Boolean algebra BΣ1[Nu 1 ].

PhD defences
Wednesday October 26, 2022, 2PM, ENS Lyon
Harriet Walsh Nouvelles classes d'universalité pour les partitions aléatoires par Harriet Walsh

PhD defences
Friday October 21, 2022, 1:30PM, Salle des thèses (580F, halle aux farines)
Hugo Moeneclaey Cubical Models Are Cofreely Parametric

A parametric model of type theory is defined as a model where any type comes with a relation and any term respects these. Intuitively, this means that terms treat their inputs uniformly. In recent years many cubical models of type theory have been proposed, often built to support some form of parametricity. In this thesis, we explain this phenomena by defending that cubical models of type theory are cofreely parametric. To do this, we define notions of parametricity and their associated parametric models, then we prove that cofreely parametric models exist, and finally we give examples of cubical models which are indeed cofreely parametric. In Chapter 1, we define the standard parametricity in details for categories and clans, with homotopically-flavored examples of parametric models. Then we give an informal survey of variants of parametricity, giving us ample potential applications for the next chapters. An important variant is internal parametricity where any type comes with a reflexive relation. In Chapter 2, we axiomatize the situation by going back to the historical approach to parametricity, namely that it is inductively proven for the initial model. So an extension by section of a theory is defined as an extension by inductively defined unary operations. This is made precise using signatures for quotient inductive-inductive types. The extensions of the theory of categories, clans and categories with families by the standard parametricity are all key examples of extensions by section. We prove that the forgetful functors coming from such extensions have right adjoints, so that cofreely parametric models exist. We also explain how to extend the standard parametricity to arrow types and universes. In Chapter 3 we give an alternative axiomatization of parametricity, that manages to give a very compact description for cofreely parametric models when applicable. We work with a symmetric monoidal closed category V of models of type theory. We define a notion of parametricity as a monoid in V, and a parametric model as a module. Then we build cofreely (and freely) parametric models as coinduced (and induced) modules. We prove that strict variants of both the category of left exact categories and the category of clans are symmetric monoidal closed. Then we prove that both the lex categories of n-truncated cubical objects and the clans of Reedy fibrant cubical objects are cofreely parametric models for suitable notions of parametricity.

PhD defences
Thursday October 20, 2022, 2PM, 3052
Daniel Szilagyi Towards efficient quantum algorithms for optimization and sampling

PhD defences
Tuesday September 20, 2022, 10AM, Salle 270 F des Halles aux Farines & Zoom
Ny Aina Andriambolamalala (IRIF) Decentralized communications and Beep model

This thesis gathers several works on distributed communication problems. In par- ticular, we focus on designing randomized distributed algorithms addressing the naming, the counting, the broadcasting and the leader election problems. The algorithms presented in this thesis are designed to resolve these problems on single- hop and multi-hop radio and beeping networks. We focus on optimizing the time complexity and the energy complexity of these algorithms. A commonly known principle for designing distributed randomized algorithms makes each device of the network decide which computation to perform in a randomized manner at each time slot of the execution of the algorithm. Hence, we propose a new paradigm, which makes each node generate some random variables distributed following a specific distribution before communicating on the network in a distributed deterministic manner. Throughout this thesis, we use several random variable distributions to resolve each problem after the other. We also propose a new witnessing paradigm to help us optimize the energy complexity of the algorithms. The first part of the thesis (the first three chapters) provides the description of the models, problems, existing algorithms and complexity measures considered in the thesis. The second part presents the new algorithms designed to resolve the considered problems.

Keywords: Distributed Computing, Initialization, Naming, Optimal, Beep, Leader Election, Energy Complexity, Broadcasting, Clustering, Time Complexity, Randomized, Radio Networks, Synchronized

PhD defences
Tuesday July 12, 2022, 9:30AM, CEA Nano innovation bat 862 ampli 33/34
Zenab Nehaï (CEA-IRIF) Formalisation et vérification des systèmes blockchain

PhD defences
Friday June 10, 2022, 12AM, Online, zoom
Yiting Jiang (IRIF and ZJNU-China) Many aspects of graph coloring

PhD defences
Tuesday May 24, 2022, 2PM, 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)$.


Year 2021

PhD defences
Wednesday December 15, 2021, 2PM, 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.

Manuscript

PhD defences
Tuesday December 14, 2021, 10AM, 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.

PhD defences
Monday December 13, 2021, 2PM, 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.

Manuscript

PhD defences
Monday December 13, 2021, 3PM, Zoom
Axel Osmond Une étude catégorique des dualités spectrales

La construction spectrale subsume plusieurs notions mathématiques d'importance, telles que le spectre d'un anneau commutatif en géométrie algébrique ou la dualité de Stone. Entremêlant des aspects catégoriques, topologiques et logiques, elle repose sur la notion de géométrie, une condition reliant un choix de théorie essentiellement algébrique, d'une extension géométrique axiomatisant une classe d'objets dits locaux, et d'un système de factorisation, encodant des situations de nature géométrique dans une catégorie d'objets algébriques. Le spectre associé à une géométrie est alors une construction permettant de déployer cette géométrie cachée d'une façon universelle. Plusieurs approches plus ou moins complètes ont été proposées en parallèle pour la construction spectrale, utilisant des formalismes très différents, les uns issue de la théorie catégoriques des modèles, d'autres purement catégoriques, d'autres reposant sur le langage des topos. Cette thèse se propose d'unifier ces différents traitements en une approche synthétique combinant les différents aspects de cette construction. Nous discutons par ailleurs en épilogue quelques éléments pour une version 2-catégorique de cette théorie permettant de retrouver les dualités syntaxe-sémantique de la logique du premier ordre comme des constructions spectrales. https://hal.archives-ouvertes.fr/tel-03609605

PhD defences
Thursday November 25, 2021, 2PM, 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.

PhD defences
Friday November 12, 2021, 2PM, 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

PhD defences
Tuesday November 9, 2021, 5PM, 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.

Manuscript

PhD defences
Friday November 5, 2021, 2PM, Bâtiment Sophie Germain
Antoine Pietri (IRIF) Organizing the graph of public software development for large-scale mining

The Software Heritage project is a software archive containing the largest public collection of source code files along with their development history, in the form of an immense graph of hundreds of billions of edges. In this thesis, we present architectural techniques to make this graph available for research. We first propose some utilities to access the data at a micro-level in a way that is convenient for smaller-scale research. To run analyses on the entire archive, we extract a property graph in a relational format and evaluate the different ways this data can be exploited using in-house and cloud processing services. We find that while this approach is well suited to process large amounts of flat data in parallel, it has inherent limitations for the highly-recursive graph structure of the archive. We propose the use of graph compression as way to considerably reduce the memory usage of the graph, allowing us to load it entirely in physical memory. We develop a library to run arbitrary algorithms on the compressed graph of public development, using various mapping techniques to access properties at the node and edge levels. We then leverage this infrastructure to study the topology of the entire graph, looking at both its local properties and the way software projects are organized in forks. The in-depth understanding of this structure then allows us to experimentally test and evaluate different approaches for distributed graph analysis.

PhD defences
Friday October 22, 2021, 4PM, 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.

PhD defences
Tuesday September 28, 2021, 3PM, 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.

Manuscript

PhD defences
Monday September 27, 2021, 3PM, 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.

Manuscript

PhD defences
Wednesday July 7, 2021, 2PM, 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.

Manuscript

PhD defences
Tuesday June 29, 2021, 10AM, Amphithéâtre Alan Turing & Zoom
Rémi Nollet (IRIF) A study of circular representations of infinite proofs for fixed-points logics, their5expressiveness and complexity.

PhD defences
Monday May 24, 2021, 2PM, Bâtiment Sophie Germain
Rachid Zennou (IRIF) Méthodes algorithmiques pour la vérification de la consistance dans les systèmes distribués

PhD defences
Tuesday May 11, 2021, 3PM, 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.

PhD defences
Tuesday March 30, 2021, 4PM, 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.

PhD defences
Tuesday March 30, 2021, 9:30AM, 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.

PhD defences
Monday March 15, 2021, 2:30PM, 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.

PhD defences
Thursday January 28, 2021, 3PM, 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.

PhD defences
Friday January 8, 2021, 9:30AM, 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.


Year 2020

PhD defences
Friday December 4, 2020, 2PM, 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)}.

PhD defences
Thursday November 26, 2020, 1PM, 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.

PhD defences
Monday November 23, 2020, 10AM, 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.

PhD defences
Wednesday November 4, 2020, 3PM, 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.

PhD defences
Thursday October 15, 2020, 4PM, 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

PhD defences
Friday June 26, 2020, 2PM, 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


Year 2019

PhD defences
Tuesday December 17, 2019, 10AM, 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.

PhD defences
Monday December 16, 2019, 2:30PM, 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

PhD defences
Thursday December 12, 2019, 2PM, 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

PhD defences
Monday December 9, 2019, 2PM, 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.

PhD defences
Friday December 6, 2019, 3:30PM, 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

PhD defences
Tuesday December 3, 2019, 2:30PM, 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.

PhD defences
Monday September 30, 2019, 2PM, Bâtiment Sophie Germain
Xin Ye Model checking self modifying code

A Self modifying code is code that modifies its own instructions during execution time. It is nowadays widely used, especially in malware to make the code hard to analyse and to detect by anti-viruses. Thus, the analysis of such self modifying programs is a big challenge. Pushdown Systems (PDSs) is a natural model that is extensively used for the analysis of sequential programs because it allows to accurately model procedure calls and mimic the program’s stack. In this thesis, we propose to extend the PushDown System model with self-modifying rules. We call the new model Self-Modifying PushDown System (SM-PDS). A SM-PDS is a PDS that can modify its own set of transitions during execution. First, we show how SM-PDSs can be used to naturally represent self-modifying programs and provide efficient algorithms to compute the backward and forward reachable configurations of SM-PDSs. Then, we consider the LTL model-checking problem of self-modifying code. We reduce this problem to the emptiness problem of Self-modifying Büchi Pushdown Systems (SM-BPDSs). We also consider the CTL model-checking problem of self-modifying code. We reduce this problem to the emptiness problem of Self-modifying Alternating Büchi Pushdown Systems (SM-ABPDSs). We implement our techniques in a tool called SMODIC. We obtained encouraging results. In particular, our tool was able to detect several self-modifying malwares; it could even detect several malwares that well-known anti-viruses such as McAfee, Norman, BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Avast and Symantec failed to detect.

PhD defences
Wednesday June 26, 2019, 2PM, Bâtiment Sophie Germain
Paulina Cecchi Bernales (IRIF) Invariant measures in symbolic dynamics: a topological, combinatorial and geometrical approach

In this work we study some dynamical properties of symbolic dynamical systems, with particular emphasis on the role played by the invariant probability measures of such systems. We approach the study of the set of invariant measures from a topological, combinatorial and geometrical point of view. From a topological point of view, we focus on the problem of orbit equivalence and strong orbit equivalence between dynamical systems given by minimal actions of Z, through the study of an algebraic invariant, namely the dynamical dimension group. Our work presents a description of the dynamical dimension group for two particular classes of subshifts: S-adic subshifts and dendric subshifts. From a combinatorial point of view, we are interested in the problem of balance in minimal uniquely ergodic systems given by actions of Z. We investigate the behavior regarding balance for substitutive, S-adic and dendric subshifts. We give necessary conditions for a minimal substitutive system with rational frequencies to be balanced on its factors, obtaining as a corollary the unbalance in the factors of length at least 2 in the subshift generated by the Thue-Morse sequence. Finally, from the geometrical point of view, we investigate the problem of realization of Choquet simplices as sets of invariant probability measures associated to systems given by minimal actions of amenable groups on the Cantor set. We introduce the notion of congruent monotileable amenable group, we prove that every virtually nilpotent amenable group is congruent monotileable, and we show that for a discrete infinite group G with this property, every Choquet simplex can be obtained as the set of invariant measures of a minimal G-subshift.

PhD defences
Friday June 21, 2019, 3PM, Amphithéâtre Turing
Nikola K. Blanchard (IRIF) Usability: low tech, high security

PhD defences
Friday June 21, 2019, 3PM, Amphithéâtre Turing, Bâtiment Sophie Germain
Enka Blanchard (IRIF) Usability: low tech, high security

This dissertation deals with the field of usable security, particularly in the contexts of online authentication and verifiable voting systems.The ever-expanding role of online accounts in our lives, from social networks to banking or online voting, has led to some initially counterproductive solutions. As recent research has shown, the problem is not just technical but has a very real psychosocial component. Password-based authentication, the subject of most of this thesis, is intrinsically linked to the unconscious mechanisms people use when interacting with security systems. Everyday, users face trade-offs between protecting their security and spending valuable mental resources, with a choice made harder by conflicting recommendations, a lack of standards, and the ad-hoc constraints still frequently encountered. Moreover, as recent results from usable security are often ignored, the problem might stem from a fundamental disconnect between the users, the developers and the researchers. We try to address those problems with solutions that are not only simplified for the user's sake but also for the developer's. To this end, we use tools from cryptography and psychology, and report on seven usability experiments.The first part of the contributions uses a service provider's point of view, with two tools to improve the end-user's experience without requiring their cooperation. We start by analysing how easily codes of different structures can be transcribed, with a proposal that reduces error rates while increasing speed. We then look at how servers can accept typos in passwords without changing the general hashing protocol, and how this could improve security. The second part focuses on end-users, starting by a proposed mental password manager that only depends on remembering only a single passphrase and PIN, with guarantees on the mutual security of generated passwords if some get stolen. We also provide a better way to create such passphrases. As mental computing models are central to expanding this field, we finish by empirically showing why the main model used today is not adapted to the purpose.In the third part, we focus on voting protocols, and investigate why changing the ones used in practice is an uphill battle. We try to answer a demand for simple paper-based systems by providing low-tech versions of the first paper-based verifiable voting scheme. To conclude, we propose a set of low-tech primitives combined in a protocol that allows usable verifiable voting with no electronic means in small elections.

PhD defences
Thursday June 20, 2019, 2:30PM, 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

PhD defences
Thursday March 14, 2019, 2PM, Bâtiment Sophie Germain
Tommaso Petrucciani (IRIF) Polymorphic set-theoretic types for functional languages

We study set-theoretic types: types that include union, intersection, and negation connectives. Set-theoretic types, coupled with a suitable subtyping relation, are useful to type several programming language constructs – including conditional branching, pattern matching, and function overloading – very precisely. We define subtyping following the semantic subtyping approach, which interprets types as sets and defines subtyping as set inclusion. Our set-theoretic types are polymorphic, that is, they contain type variables to allow parametric polymorphism.We extend previous work on set-theoretic types and semantic subtyping by showing how to adapt them to new settings and apply them to type various features of functional languages. More precisely, we integrate semantic subtyping with three important language features.In Part I we study implicitly typed languages with let-polymorphism and type inference (previous work on semantic subtyping focused on explicitly typed languages). We describe an implicitly typed lambda-calculus and a declarative type system for which we prove soundness. We study type inference and prove results of soundness and completeness. Then, we show how to make type inference more precise when programs are partially annotated with types.In Part II we study gradual typing. We describe a new approach to add gradual typing to a static type system; the novelty is that we give a declarative presentation of the type system, while previous work considered algorithmic presentations. We first illustrate the approach on a Hindley-Milner type system without subtyping. We describe declarative typing, compilation to a cast language, and sound and complete type inference. Then, we add set-theoretic types, defining a subtyping relation on set-theoretic gradual types, and we describe sound type inference for the extended system.In Part III we consider non-strict semantics. The existing semantic subtyping systems are designed for call-by-value languages and are unsound for non-strict semantics. We adapt them to obtain soundness for call-by-need. To do so, we introduce an explicit representation for divergence in the types, allowing the type system to distinguish the expressions that are already evaluated from those that are computations which might diverge.


Year 2018

PhD defences
Friday December 7, 2018, 2PM, Salle François Jacob, bâtiment Buffon
Pierre Cagne (IRIF) Towards a homotopical algebra of dependent types

PhD defences
Friday November 30, 2018, 2:30PM, 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.

PhD defences
Friday November 23, 2018, 2PM, 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.

PhD defences
Friday October 19, 2018, 9:30AM, 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.

PhD defences
Thursday September 27, 2018, 3:30PM, 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.

PhD defences
Wednesday September 26, 2018, 2PM, Bâtiment Sophie Germain
Vitalii Aksenov (IRIF) Synchronization costs in parallel programs and concurrent data structures

To use the computational power of modern computing machines, we have to deal with concurrent programs. Writing efficient concurrent programs is notoriously difficult, primarily due to the need of harnessing synchronization costs. In this thesis, we focus on synchronization costs in parallel programs and concurrent data structures.First, we present a novel granularity control technique for parallel programs designed for the dynamic multithreading environment. Then in the context of concurrent data structures, we consider the notion of concurrency-optimality and propose the first implementation of a concurrency-optimal binary search tree that, intuitively, accepts a concurrent schedule if and only if the schedule is correct. Also, we propose parallel combining, a technique that enables efficient implementations of concurrent data structures from their parallel batched counterparts. We validate the proposed techniques via experimental evaluations showing superior or comparable performance with respect to state-of-the-art algorithms.From a more formal perspective, we consider the phenomenon of helping in concurrent data structures. Intuitively, helping is observed when the order of some operation in a linearization is fixed by a step of another process. We show that no wait-free linearizable implementation of stack using read, write, compare&swap and fetch&add primitives can be help-free, correcting a mistake in an earlier proof by Censor-Hillel et al. Finally, we propose a simple way to analytically predict the throughput of data structures based on coarse-grained locking.

PhD defences
Tuesday September 25, 2018, 2PM, 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.

PhD defences
Thursday September 20, 2018, 10AM, 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.

PhD defences
Wednesday September 19, 2018, 2PM, 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.

PhD defences
Tuesday September 18, 2018, 2PM, 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.

PhD defences
Monday September 10, 2018, 2PM, 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.

PhD defences
Monday September 10, 2018, 2PM, Bâtiment Sophie Germain
Bin Fang (IRIF) Techniques for formal modelling and verification on dynamic memory allocators

The first part of the thesis demonstrates how to obtain formal specifications of free-list SDMA using a refinement-based approach. The thesis defines a hierarchy of models ranked by the refinement relation that capture a large variety of techniques and policies employed by real-work SDMA. This hierarchy forms an algorithm theory for the free-list SDMA and could be extended with other policies. The formal specifications are written in Event-B and the refinements have been proved using the Rodin platform. The thesis investigates applications of the formal specifications obtained, such as model-based testing, code generation and verification.The second part of the thesis defines a technique for inferring precise invariants of existing implementations of SDMA based abstract interpretation. For this, the thesis defines an abstract domain representing sets of states of the SDMA. The abstract domain is based on a fragment of Separation Logic, called SLMA. This fragment captures properties related with the shape and the content of data structures used by the SDMA to manage the heap. The abstract domain is defined as a specific product of an abstract domain for heap shapes with an abstract domain for finite arrays of locations. To obtain compact elements of this abstract domain, the thesis proposes an hierarchical organisation of the abstract values: a first level abstracts the list of all chunks while a second level selects only the chunks available for allocation. The thesis defines transformers of the abstract values that soundly capture the semantics of statements used in SDMA implementations. A prototype implementation of this abstract domain has been used to analyse simple implementations of SDMA.

PhD defences
Thursday July 5, 2018, 2:30PM, 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.

PhD defences
Thursday July 5, 2018, 2PM, Room B107 of LIPN, Université Paris 13
Huu Vu Nguyen (IRIF) On CARET Model-Checking of Pushdown Systems: Application to Malware Detection

The number of malware is growing significantly fast. Traditional malware detectors based on signature matching or code emulation are easy to get around. To overcome this problem, model-checking emerges as a technique that has been extensively applied for malware detection recently. Pushdown systems were proposed as a natural model for programs, since they allow to keep track of the stack, while extensions of LTL and CTL were considered for malicious behavior specification. However, LTL and CTL like formulas don't allow to express behaviors with matching calls and returns. In this thesis, we propose to use CARET (a temporal logic of calls and returns) for malicious behavior specification. CARET model checking for Pushdown Systems (PDSs) was never considered in the literature. Previous works only dealt with the model checking problem for Recursive State Machine (RSMs). While RSMs are a good formalism to model sequential programs written in structured programming languages like C or Java, they become non suitable for modeling binary or assembly programs, since, in these programs, explicit push and pop of the stack can occur. Thus, it is very important to have a CARET model checking algorithm for PDSs. We tackle this problem in this thesis. We reduce it to the emptiness problem of Büchi Pushdown Systems. Since CARET formulas for malicious behaviors are huge, we propose to extend CARET with variables, quantifiers and predicates over the stack. This allows to write compact formulas for malicious behaviors. Our new logic is called Stack linear temporal Predicate logic of CAlls and RETurns (SPCARET). We reduce the malware detection problem to the model checking problem of PDSs against SPCARET formulas, and we propose efficient algorithms to model check SPCARET formulas for PDSs. We implemented our algorithms in a tool for malware detection. We obtained encouraging results. We then define the Branching temporal logic of CAlls and RETurns (BCARET) that allows to write branching temporal formulas while taking into account the matching between calls and returns and we proposed model-checking algorithms of PDSs for BCARET formulas. Finally, we consider Dynamic Pushdown Networks (DPNs) as a natural model for multithreaded programs with (recursive) procedure calls and thread creation. We show that the model-checking problem of DPNs against CARET formulas is decidable.

PhD defences
Thursday July 5, 2018, 10AM, Salle B107 du LIPN, Université Paris 13
Adrien Pommellet (IRIF) On Model-checking Pushdown System Models

In this thesis, we propose different model-checking techniques for pushdown system models. Pushdown systems (PDSs) are indeed known to be a natural model for sequential programs, as they feature an unbounded stack that can simulate the assembly stack of an actual program. Our first contribution consists in model-checking the logic HyperLTL that adds existential and universal quantifiers on path variables to LTL against pushdown systems (PDSs). The model-checking problem of HyperLTL has been shown to be decidable for finite state systems. We prove that this result does not hold for pushdown systems nor for the subclass of visibly pushdown systems. Therefore, we introduce approximation algorithms for the model-checking problem, and show how these can be used to check security policies. In the second part of this thesis, as pushdown systems can fail to accurately represent the way an assembly stack actually operates, we introduce pushdown systems with an upper stack (UPDSs), a model where symbols popped from the stack are not destroyed but instead remain just above its top, and may be overwritten by later push rules. We prove that the sets of successors post* and predecessors pre* of a regular set of configurations of such a system are not always regular, but that post* is context-sensitive, hence, we can decide whether a single configuration is forward reachable or not. We then present methods to overapproximate post* and under-approximate pre*. Finally, we show how these approximations can be used to detect stack overflows and stack pointer manipulations with malicious intent. Finally, in order to analyse multi-threaded programs, we introduce in this thesis a model called synchronized dynamic pushdown networks (SDPNs) that can be seen as a network of pushdown processes executing synchronized transitions, spawning new pushdown processes, and performing internal pushdown actions. The reachability problem for this model is obviously undecidable. Therefore, we compute an abstraction of the execution paths between two regular sets of configurations. We then apply this abstraction framework to a iterative abstraction refinement scheme.

PhD defences
Tuesday July 3, 2018, 2PM, Room B107 of LIPN, Université Paris 13
Khanh Huu The Dam (IRIF) Automatic Learning and Extraction of Malicious Behaviors

Malware detection is nowadays a big challenge. The existing techniques for malware detection require a huge effort of engineering to manually extract the malicious behaviors. To avoid this tedious task of manually discovering malicious behaviors, we propose in this thesis two approaches: (1) Apply Information Retrieval techniques to automatically discover malicious behaviors, and (2) Apply machine learning to automatically learn malwares. We use API call graphs to represent programs. API call graphs are graphs whose nodes are API functions and whose edges represent the order of execution of the different calls to the API functions (i.e, functions supported by the operating system). To automatically learn malwares, we apply well-known learning techniques based on Random Walk Graph Kernels (combined with Support Vector Machines). We achieve a high detection rate with only few false alarms (97% for detection rate with 0.73% of false alarms). As for the automatic extraction of malicious behaviors, we reduce this problem to the problem of retrieving from the benign and malicious API call graphs the set of subgraphs that are relevant for malicious behaviors. We solve this issue by applying and adapting well-known efficient Information Retrieval techniques based on the TFIDF scheme. We use our automatically extracted malicious behavior specification for malware detection using a kind of product between graphs. We obtained interesting experimental results, as we get 96% of detection rate. Using our two approaches, we were able to detect several malwares that well-known and widely used antiviruses such as Panda, Avira, Kaspersky, Avast, Qihoo360, McAfee, AVG, BitDefender, ESET-NOD32, F-Secure and Symantec could not detect.

PhD defences
Tuesday July 3, 2018, 2PM, Salle 580F (Halle aux Farines)
Thibaut Girka (IRIF) Differential program semantics

Computer programs are rarely written in one fell swoop. Instead, they are written in a series of incremental changes.It is also frequent for software to get updated after its initial release. Such changes can occur for various reasons, such as adding features, fixing bugs, or improving performances for instance. It is therefore important to be able to represent and reason about those changes, making sure that they indeed implement the intended modifications.In practice, program differences are very commonly represented as textual differences between a pair of source files, listing text lines that have been deleted, inserted or modified. This representation, while exact, does not address the semantic implications of those textual changes. Therefore, there is a need for better representations of the semantics of program differences.Our first contribution is an algorithm for the construction of a correlating program, that is, a program interleaving the instructions of two input programs in such a way that it simulates theirsemantics. Further static analysis can be performed on such correlating programs to compute an over-approximation of the semantic differences between the two input programs. This work draws direct inspiration from an article by Partush and Yahav, that describes a correlating program construction algorithm which we show to be unsound on loops that include `break` or `continue`statements. To guarantee its soundness, our alternative algorithm is formalized and mechanically checked within the Coq proof assistant.Our second and most important contribution is a formal framework allowing to precisely describe and formally verify semantic changes.This framework, fully formalized in Coq, represents the difference between two programs by a third program called an oracle.Unlike a correlating program, such an oracle is not required to interleave instructions of the programs under comparison, and may “skip” intermediate computation steps. In fact, such an oracle is typically written in a different programming language than the programs it relates, which allows designing correlating oracle languages specific to certain classes of program differences, andcapable of relating crashing programs with non-crashing ones.We design such oracle languages to cover a wide range of program differences on a toy imperative language. We also prove that our framework is at least as expressive as Relational Hoare Logic by encoding several variants as correlating oracle languages, proving their soundness in the process.

PhD defences
Friday June 15, 2018, 2PM, Bâtiment Sophie Germain
Clément Dervieux (IRIF) Enumeration of oriented planar maps

After a general presentation of planar maps, we define corner polyhedra, studied by Eppstein and Mumford. We soon introduce corner triangulations, that are dual maps of the skeletons of corner polyhedra, and we give some properties of them.We offer a linear time algorithm to realize corner polyhedra. For that, the study of corner triangulations leads to enumeration problems. A classic method, known from Tutte, gives the wanted result, making the series of Catalan numbers appearing. The research for a combinatorial explanation of the presence of Catalan numbers induces the use of other methods, based on cuttings and gluings of some parts of corner triangulations. Thus appears the family of almond triangulations, that is a new representation of Catalan numbers, in bijection with the binary trees family, and that completes our corner polyhedra realization algorithm. We eventually give a conclusion to these works, trying to generalize our methods to maps whose faces have an any fixed degree.

PhD defences
Friday May 25, 2018, 3PM, Salle 0010, Bâtiment Sophie Germain
Florent Urrutia (IRIF) Information Theory for Multi-Party Peer-to-Peer Communication Protocols

This thesis is concerned with the study of multi-party communicationprotocols in the asynchronous message-passing peer-to-peer model. We introducetwo new information measures, the Public Information Complexity(PIC) and the Multi-party Information Complexity (MIC), study their propertiesand how they are related to other fundamental quantities in distributedcomputing such as communication complexity and randomness complexity.We then use these two measures to study the parity function and the disjointness function.

PhD defences
Friday April 27, 2018, 2PM, 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


Year 2017

PhD defences
Tuesday December 12, 2017, 2:30PM, 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

PhD defences
Thursday December 7, 2017, 2:30PM, Amphi 10E, Halle aux Farines
Pierre Vial (IRIF) Non-idempotent typing operators, beyond the lambda-calculus

L'objet de cette thèse est l'extension des méthodes de la théorie des types intersections non-idempotents, introduite par Gardner et de Carvalho, à des cadres dépassant le lambda-calcul stricto sensu.
  • Nous proposons d'abord une caractérisation de la normalisation de tête et de la normalisation forte du lambda-mu calcul (déduction naturelle

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

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

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

PhD defences
Friday December 1, 2017, 2:30PM, Salle des Thèses, Halle aux Farines
Maxime Lucas (IRIF) Cubical categories for homotopy and rewriting

PhD defences
Friday November 17, 2017, 3:15PM, Salle 153, Olympe de Gouges
Etienne Miquey (IRIF) Classical realizability and side-effects

PhD defences
Tuesday November 14, 2017, 11AM, Salle des Thèses, Halle aux Farines
Gabriel Radanne (IRIF) Tierless Web programming in ML

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

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

PhD defences
Friday September 1, 2017, 10AM, Salle 2014, Bâtiment Sophie Germain
Jovana Obradović (IRIF) Cyclic operads: syntactic, algebraic and categorified aspects

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

PhD defences
Thursday July 13, 2017, 2:30PM, Amphithéâtre Turing, Bâtiment Sophie Germain
Thibault Godin (IRIF) Mealy machines, automaton (semi)groups,decision problems and random generation

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

PhD defences
Friday July 7, 2017, 2PM, Salle 0010, Bâtiment Sophie Germain
Bruno Karelovic (IRIF) Quantitative analysis of stochastic systems : priority games and populations of Markov chains

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

PhD defences
Tuesday June 27, 2017, 10AM, Salle 255, Olympe de Gouges
Amina Doumane (IRIF) On the infinitary proof theory of logics with fixed points

PhD defences
Tuesday February 7, 2017, 4PM, Amphithéâtre Turing, Bâtiment Sophie Germain
Mathieu Lauriere (IRIF) Complexites de communication et d'information dans les modèles classique et quantique


Year 2016

PhD defences
Friday December 9, 2016, 2PM, 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

PhD defences
Tuesday October 11, 2016, 2PM, Salle 1006, Sophie Germain
Wenjie Fang (IRIF) Aspects énumératifs et bijectifs des cartes combinatoires : généralisation, unification et application

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

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

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

PhD defences
Friday April 8, 2016, 10AM, Salle 2011, Sophie Germain
Charles Grellois (IRIF) Sémantique de la logique linéaire et model-checking d'ordre supérieur