As the title suggests, this thesis is an exploration of the bijective links between three families of combinatorial objects: planar maps, Tamari intervals and parking trees. Along the way, we will encounter many other kinds of combinatorial animals with exotic names, such as fighting fish, quadrant excursions, embedded mobiles, closed flows and blossoming trees…
Planar maps have been well known to combinatorialists since they were intro- duced about sixty years ago. Their rich underlying combinatorial structure has contributed to the development of a strong bijective framework surrounding them. We can cite the examples of bijections with blossoming trees, which allow elegant proofs of beautiful formulas counting families of planar maps. More recently, the discovery of similar formulas for Tamari intervals has led to the exploration of the bijective connection with planar maps. In this manuscript, we revisit some of these bijections and create new ones, shedding new light by integrating numerous combi- natorial families.
At the crossroads of the correspondences developed in our work, we will en- counter several models of parking trees. Not only do these trees appear naturally to encode families of planar maps and Tamari intervals, but they are also proto- types of objects governed by catalytic equations. In this sense, the general study of parking trees, initiated by Duchi and Schaeffer in 2023, and continued here, seems very promising for a further refined understanding of the bijective and enumerative schemes surrounding this manuscript.

This manuscript focuses on defining and optimizing code-based cryptographic primitives, with a particular emphasis on digital signatures derived through the Fiat-Shamir transformation of zero-knowledge proofs of knowledge. It presents three main contributions.
The first contribution introduces a five-round zero-knowledge proof of knowledge protocol based on the RSD problem, employing an advanced witness conversion technique. The protocol is then transformed into a digital signature scheme using the Fiat-Shamir heuristic, adapted for post-quantum security. Performance is further optimized through a novel hypercube technique, achieving competitive speeds relative to existing schemes. The second contribution focuses on improving the efficiency of the MPC-in-the-Head paradigm by defining multi-instance puncturable pseudorandom functions (PPRFs) specifically designed for code-based protocols: replacing traditional hash-based approaches with fixed-key block ciphers, the proposed PPRFs reduce signing and verification times by up to 55×, establishing new performance benchmarks for MPC-in-the-Head-based schemes.
The third contribution extends the initial digital signature scheme into a threshold signature framework, addressing the challenges of efficiently adapting MPC-based schemes for multi-user collaborative signing. The proposed methodology minimizes the trade-off between signature size and user count, outperforming naive concatenation techniques. Applied to the earlier code-based signature scheme, this approach results in a practical and efficient threshold signature solution.
In conclusion, this manuscript presents significant advancements in code-based post-quantum cryptography by addressing fundamental challenges in security and efficiency. Combining rigorous theoretical design with practical relevance, the contributions align with the goals of the NIST standardization process and address emerging needs such as blockchain and decentralized systems.

In this thesis, we put forward advancements in Multi-Party Computation (MPC), enabling parties to jointly compute arbitrary functions while preserving the privacy of their inputs. Our focus is on MPC with correlated randomness, where efficiency is improved through correlations generated using preprocessing. We investigate two key paradigms for generating such randomness: Pseudorandom Correlation Generators (PCGs) and Pseudorandom Correlation Functions (PCFs). First, we propose new PCG-based constructions for Private Set Intersection (PSI), achieving either tighter security or improved performance. We then explore the applications of PCGs and PCFs in Zero-Knowledge Proofs (ZKPs), addressing both interactive and non-interactive settings. For interactive ZKPs, we design a privately verifiable protocol for circuit satisfiability with sublinear communication and efficient computation. In the non-interactive setting, we introduce a new designated-verifier ZKP (DV-NIZK) leveraging PCF with a public-key structure (PK-PCF). Finally, we introduce a novel MPC framework for binary circuits, utilizing a PCG optimized for small fields.

The connection between logic and computer science has been fruitfully explored for years, and yet there is still so much to uncover. This thesis aims to further enrich this fascinating field by delving into the interplay between the ecosystem of linear logic and that of programming languages. In the first part, we introduce a new definition of parallel cut elimination for multiplicative-exponential linear logic (MELL) proof nets. Drawing inspiration from Tait and Martin-Löf’s parallel reduction in the lambda calculus, we address the challenges posed by untyped proof nets by defining a generalized notion of substitution on more abstract structures called prestructures. This approach allows us to define parallel exponential cut elimination for MELL prestructures in a rigorous and systematic way. Through the strong confluence of this operation, we provide a confluence proof for cut elimination in MELL proof nets without relying on Newman’s lemma or strong normalization. Furthermore, we extend this framework to define complete parallel cut elimination, offering an alternative confluence proof that closely mirrors Tait and Martin-Löf’s approach for the lambda calculus. The second part of this work introduces a new logic system, PiL, which extends first-order multiplicative and additive linear logic by incorporating a non-commutative, non-associative connective and nominal quantifiers. We prove that PiL enjoys cut elimination and embed the recursion-free fragment of the pi-calculus within PiL, demonstrating that the operational semantics of the pi-calculus can be captured by linear implication in PiL. This result allows us to characterize key properties such as deadlock freedom, ensuring that a network of processes can continue executing until termination, and progress, particularly for systems without mobility.Additionally, we establish a choreographies-as-proofs correspondence, providing the first completeness theorem for choreographies within this fragment of the pi-calculus. Finally, we introduce proof nets for PiL by integrating techniques from conflict nets and unification nets, thereby defining the first syntax for conflict nets in the context of multiplicative-additive linear logic with first-order quantifiers. By linking computation trees to derivations and deriving canonical representatives of these trees in the same manner as proof nets represent sequent calculus proofs, this work opens new avenues for bridging computation and logic.

The growth of modern internet is enabled by large-scale, highly available, and resilient distributed systems. These systems allow data to be replicated globally while ensuring availability under failures. To ensure reliability and availability in the presence of failures, the systems rely on intricate distributed protocols. Yet in practice, bugs in the implementations of these distributed protocols have been the source of many downtimes in popular distributed databases. Ensuring the correctness of the implementations remains a significant challenge due to the large state space.

Over the years, many techniques have been developed to ensure the correctness of the implementations ranging from systematic model checking to pure random exploration. However, a developer testing the implementation with current techniques has no control over the exploration. In effect, the techniques are agnostic to the developer's knowledge of the implementation. Furthermore, very few approaches utilize the formal models of the protocols when testing the implementations. Efforts put into modeling and verifying the correctness of the model are not leveraged to ensure the correctness of the implementation

To address these drawbacks, in this thesis, we propose 3 new approaches to test distributed protocol implementations - Netrix, WaypointRL, and ModelFuzz. The first two techniques - Netrix and WaypointRL are biased exploration approaches that accept developer input. Netrix is a novel unit testing algorithm that allows developers to bias the exploration of an existing testing algorithm. A developer writes low-level filters in a domain-specific language to fix specific events in an execution that are enforced by Netrix. WaypointRL improves on Netrix to accept high-level state predicates as waypoints and uses reinforcement learning to satisfy the predicates. WaypointRL is effective in biasing the exploration while requiring less effort from the developer. Using popular distributed protocol implementations, we show that additional developer input leads to effective biased exploration and improved bug-finding capabilities. The third technique - ModelFuzz - is a new fuzzing algorithm that bridges the gap between the model and the implementation of the protocol. We use model states as coverage to guide input generation that are then executed on the implementation. We show with three industrial benchmarks that existing coverage notions are insufficient for testing distributed systems and that using TLA+ model coverage to test implementations leads to discovering new bugs.

Distributed computing encompasses all models where a set of computing entities have to collectively solve a problem while each detaining private inputs. This field of theoretical computer science then underlies many real situations: multi-core processors, servers and clouds, the internet, swarms of robots, cars or other intelligent objects, and any network in which entities have some kind of independence. This thesis is dedicated to studying the impact of limited bandwidth on the ability to solve “local problems” in distributed networks. More precisely, in a graph-network where the amount of information exchanged between two neighbors is limited over time, how long does it take to detect a cycle ?

First we study a state of the art algorithm for the detection of small even cycles and show that this technique becomes unefficient for bigger lengths of cycles. For any even length of cycle bigger than 10, there exists a family of graphs of growing size in which this technique cannot detect a cycle in a reasonable time.

Then, we exhibit a new algorithm that matches and extends the complexity of the previously mentioned one to all even lengths of cycles. To prove its correctness, we establish a general graph combinatorics result. It can be seen as a lower bound of the “local density” in a graph without a 2k-cycle.

Finally, we develop a new framework for quantum distributed computing: the distributed quantum Monte-Carlo amplification. It helps us quantumly speed up our even-length cycle detection algorithm. This same technique can also be applied to speed up other cycle detection problems in the litterature.

In its first part, this thesis focuses on the study of the ramified analytic hierarchy (RAH) in second-order arithmetic (PA2). The ramified analytic hierarchy was defined by Kleene in 1960. It is an adaptation of the notion of constructibility (introduced by G¨odel for set theory) to the framework of second-order arithmetic. The properties of this hierarchy, in relation to computability and to the study of set-theoretic models of PA2, have been studied in depth. It seems natural to formalize RAH in PA2 in an attempt to demonstrate that adding the axiom of choice or (a variant of) the axiom of constructibility to second-order arithmetic does not bring contradiction. However, the only written trace of such a formalization seems to be incorrect. In this thesis, we want to work on this formalization. To do this, we will work in a version of arithmetic obtained by removing the axiom of induction from the axioms of PA2. In this system, a new variant of the axiom of choice appears: we call it the axiom of collection, in reference to the homonymous axiom of set theory. It seems that this axiom has never been considered in the context of second-order logic. We show that it has good computational properties: its contrapositive is realized by the identity in classical realizability, while it is itself realized by the identity in intuitionistic realizability. In addition, we show that it is equivalent to an axiom which is well-behaved with respect to a negative translation from classical logic into intuitionistic logic. Finally, we show that this variant of the axiom of collection is weaker than a variant of the axiom of choice in intuitionistic logic. We therefore work in a theory without induction but containing the axiom of collection. We aim at studying the ramified analytic hierarchy. We show that it is a model of PA2 satisfying a strong version of the axiom of choice: the principle of the well-ordered universe. It seems that the axiom of collection is necessary to prove this result and we will thoroughly explain this intuition.
In the second part of the thesis, shorter than the first, we study extensional equality in finite type arithmetic. Higher Type Arithmetic (HA^ω) is a first-order many-sorted theory. It is a conservative extension of Heyting Arithmetic obtained by extending the syntax of terms to all of System T: the objects of interest here are the functionals of higher types. While equality between natural numbers is specified by the axioms of Peano, how can equality between functionals be defined? From this question, different versions of HA^ω arise, such as an extensional version (E-HA^ω) and an intentional version (I-HA^ω). In this work, we will see how the study of partial equivalence relations leads us to design a translation by parametricity from E-HA^ω to HA^ω.

This thesis discusses the paradigm of computation with partial information, which is necessitated by the infeasibility of processing massive datasets in their entirety. Traditional algorithms, which require full access to input data, become impractical for large-scale problems due to time and space constraints. Several models of computation that allow for partial or incomplete data access, such as property testing, data stream models, distributed computing, and massively parallel computing, have been proposed in the literature. This thesis deals with two models, the distributed LOCAL model and the data stream model in this paradigm.

In the LOCAL model, we extend existing frameworks for the well-studied problem of $(\Delta+1)$-proper coloring to a more generalized $k$-partial $(k+1)$-coloring problem, providing novel algorithms and complexity results. Given a $n$-node graph $G=(V,E)$, a $k$-partial $c$-coloring asks for a coloring of the vertices with colors in $\{1,\dots,c\}$, such that every vertex $v\in V$ has at least $\min\{k,\deg(v)\}$ neighbors with a color different from its own color. We extend the rounding based algorithm of Ghaffari and Kuhn (2020), to give a $O(\log n\cdot \log^3k)$ round algorithm and a $O(\log n\cdot \log^2k)$ round algorithm for $k$-partial list coloring and $k$-partial $(k+1)$-coloring respectively.

In the data stream model, we introduce the {\em certification} of solutions to computing problems when access to the input is restricted. This topic has received a lot of attention in the distributed computing setting, and we introduce it here in the context of \emph{streaming} algorithms, where the input is too large to be stored in memory. Given a property $P$, a \emph{streaming certification scheme} for $P$ is a \emph{prover-verifier} pair where the prover is a computationally unlimited but non-trustable oracle, and the verifier is a streaming algorithm. For any input, the prover provides the verifier with a \emph{certificate}. The verifier then receives its input as a stream in an adversarial order and must check whether the certificate is indeed a \emph{proof} that the input satisfies $P$. The main complexity measure for a streaming certification scheme is its \emph{space complexity}, defined as the sum of the size of the certificate provided by the oracle, and of the memory space required by the verifier. We give streaming certification schemes for several graph properties, including maximum matching, diameter, degeneracy, and coloring, with space complexity matching the requirement of \emph{semi-streaming}, i.e., with space complexity $O(n\, \mbox{polylog}\, n)$ for $n$-node graphs. For each of these properties, we provide upper and lower bounds on the space complexity of the corresponding certification schemes, many being tight up to logarithmic multiplicative factors. We also show that some graph properties are hard for streaming certification, in the sense that they cannot be certified in semi-streaming, as they require $\Omega(n^2)$-bit certificates.

The results presented in this thesis contribute to the growing body of work on algorithms for large datasets, particularly in the contexts of graph theory and distributed systems, and open new avenues for future research in computation with partial information.

In the last 50 years, the amount and complexity of information stored in databases has grown and the needs of database users have evolved. These changes have led to the creation of new models such as XML, key-value stores, time series databases and so on. The subject of this thesis is one such model: the graph database. In a graph database, data is stored as a “graph”, or a collection of nodes, representing the entities, connected together by edges, representing relationships between the entities. Additional information about the entities and their relationships can be attached to the nodes and edges. This powerful model, popularized by Neo4j in 2010, is now a staple in various industries such as biology, social networks and banking. By putting the links between the data points front and center, graph databases allow users to reason not only about individual elements but also about the structure of the graph. Accordingly, the goal of a typical graph query is to find a “path” connecting specific nodes.

Because graph traversals inherently rely on transitivity, traditional query languages are not suitable in the graph context, and thus new languages have been created. In the theoretical community, the basic building blocks of a graph language are the Regular Path Queries (RPQs), which define path constraints by way of regular expressions. The expressive power and complexity of RPQs and their extensions (by union, conjunction, two-way navigation, data value comparisons and path properties for example) have been studied since the 1990s but their properties are barely beginning to be understood.

The most popular practical graph language today is Neo4j’s Cypher. In Cypher, a path can be described by a regular expression but it also includes many other features among which aggregation, different path semantics, projection, subqueries and updates. These elements differ from those of other languages, like Tigergraphs’ GSQL, or Oracle’s PGQL, but all graph systems share the same kernel: pattern matching.

In 2019, a new International Organisation for Standardization (ISO) group was created to oversee the standardization of practical graph languages. This led to two new standards: SQL/PGQ and GQL. The idea of SQL/PGQ is to add a view-based pattern matching mechanism to SQL and interpret the relational data as a graph only when necessary, whereas GQL is standalone and stores the data as a native graph. While this standardization work is a step in the right direction, there is one crucial ingredient missing: a corresponding theoretical model.

The goal of this thesis is to define a theoretical language for graph databases, akin to relational algebra for SQL, that reflects the essential aspects of GQL and SQL/PGQ while being simple enough for theoretical study. We start by presenting in detail the pattern matching features shared by SQL/PGQ and GQL. We then identify and formalize the core of this language. Afterwards, we position our formalisations of SQL/PGQ and GQL in comparison to relational algebra, which allows us to highlight their distinct styles, while also proving their equivalence. Finally, we explore the impact of extending pattern matching with list functions and show that this addition is not only dangerous in theory, but also fails in practice.

The development of applications with spreadsheets by non-professional programmers is a widespread practice both in industrial settings and in certain research fields. Owing to their simplicity and interactivity, spreadsheets count as a significant part of software development today. However, they can also be seen as poorly structured programs prone to committing programming errors.

This thesis proposes a new perspective on spreadsheet development by adopting the principles of structured programming. Through the development of Lisa, a domain specific language, we propose the structured programming approach for spreadsheets. The main feature of this approach is to organise the sheets by columns rather than by cells. In this way, we can model the columns as potentially infinite streams of data. The unique aspect of this language is the introduction of indexed streams. In this context, the indexed nature of the streams capture the notion of the current row number of a given column’s cell. A relative access (relative to the current index) operation allows preserving a programming style akin to that of formulae found in traditional spreadsheets. The remainder of the thesis addresses the design and implementation of Lisa, a functional language focused on programming with indexed streams. In particular, we cover the compilation of Lisa into executables for various execution targets, ranging from traditional hardware platforms to the blockchain. Moreover, the programs issued by the compilation process depend on a runtime environment providing the relative access operator and indexed streams. The implementation of this operation is particularly slow for classical implementations of streams. To address these performance issues, we propose a new way of programming streams that is well suited to accelerating this key operation.

Lisa is a fundamental component for the design of a specialised spreadsheet software tailored for the development of structured spreadsheets. In such a spreadsheet software, Lisa is used both to implement the formulae of a sheet and to develop extensions in the form of macro definitions. Finally, the compiled approach allows generating, from a structured sheet, an executable compatible with various software interfaces, thus enabling the modular composition of spreadsheet application developments, carried by end users, with highly technical software components developed by specialists.

Since the beginning of modern cryptography, the question of secure computation (MPC) has been extensively studied. MPC allows for a set of parties to perform some joint computation while ensuring that their input remains secure up to what is implied by the output. The massive development of our daily Internet usage makes the need for secure computation methods more urgent: computations on private data is everywhere, from recommendation algorithms to electronic auctions. Modern MPC algorithms greatly benefit from correlated randomness to achieve fast online protocols. Correlated randomness has to be massively produced beforehand for the MPC protocols to work best, and this is still a challenge to do efficiently today.

In this thesis, we study pseudorandom correlation generators (PCGs). This construction transforms a small amount of correlated randomness into a large amount of correlated pseudorandomness with minimal interaction and local computation. We present different PCG constructions whose security relies on variants of the Syndrome Decoding (SD) assumption, a classical assumption in coding theory. The intuition behind these constructions is to merge the SD assumption with some MPC techniques that enable additively sharing sparse vectors. We achieve state-of-the-art results regarding secure computation protocols requiring more than two players when the computation is over a finite field of size > 2. We show how to remove this constraint at the cost of a small overhead in communication.

Next, we consider the construction of pseudorandom correlation functions (PCFs). PCFs produce correlations on-the-fly: players each hold correlated functions such that the outputs of the functions, when evaluated on the same entry, are correlated. These objects offer more flexibility than PCGs but are also harder to construct. We again rely on variants of SD to construct PCFs. We build on a previous PCF construction, showing that the associated proof of security was incorrect, and propose a correction. Additionally, we present optimizations of the construction, coming from a better analysis and precise optimization of parameters via simulations. We achieve parameters usable in practice.

Finally, this thesis revolves around the use of certain codes, particularly the SD assumption. The search for good complexity entails efforts to find the most efficient codes while ensuring that security is not compromised. We consider a framework tailored to the study of promising attacks on SD and its variants. For each construction previously mentioned, we conduct a thorough security analysis of the associated variant of SD and attempt cryptanalysis efforts to compute concrete parameters.

Polynomial models are ubiquitous in computer science, arising in the study of automata and formal languages, optimisation, game theory, control theory, and numerous other areas. In this thesis, we consider models described by polynomial systems of equations and difference equations, where the system evolves through a set of discrete time steps with polynomial updates at every step. We explore three aspects of “zero problems” for polynomial models: zero testing for algebraic expressions given by polynomials, determining the existence of zeros for polynomial systems and determining the existence of zeros for sequences satisfying recurrences with polynomial coefficients.

In the first part, we study identity testing for algebraic expressions involving radicals. That is, given a k-variate polynomial represented by an algebraic circuit and k real radicals, we examine the complexity of determining whether the polynomial vanishes on the radical input. We improve on the existing PSPACE bound, placing the problem in coNP assuming the Generalised Riemann Hypothesis (GRH). We further consider a restricted version of the problem, where the inputs are square roots of odd primes, showing that it can be decided in randomised polynomial time assuming GRH.

We next consider systems of polynomial equations, and study the complexity of determining whether a system of polynomials with polynomial coefficients has a solution. We present a number-theoretic approach to the problem, generalising techniques used for identity testing, showing the problem belongs to the complexity class AM assuming GRH. We discuss how the problem relates to determining the dimension of a complex variety, which is also known to belong to AM assuming GRH.

In the final part of this thesis, we turn our attention to sequences satisfying recurrences with polynomial coefficients. We study the question of whether zero is a member of a polynomially recursive sequence arising as a sum of two hypergeometric sequences. More specifically, we consider the problem for sequences where the polynomial coefficients split over the field of rationals Q. We show its relation to the values of the Gamma function evaluated at rational points, which allows to establish decidability of the problem under the assumption of the Rohrlich-Lang conjecture. We propose a different approach to the problem based on studying the prime divisors of the sequence, allowing us to establish unconditional decidability of the problem.

Programming languages can be broadly categorized into two groups: static languages, such as C, Rust, and OCaml, and dynamic languages, such as Python, JavaScript, and Elixir. While static languages generally offer better performance and more security thanks to a phase of static typing that precedes compilation (“well-typed programs cannot go wrong”), this often comes at the expense of flexibility, making programs safer but prototyping more tedious. In this defense, I present a formal system for statically typing dynamic languages, offering a compromise between safety and flexibility.

Statically typing dynamic languages poses new challenges. In particular, functions in dynamic languages can be overloaded: they can express multiple behaviors that cannot be resolved statically, but are instead selected at runtime (either by explicit type-cases or by built-in dynamic dispatch). In addition, programs typically have no (or few) type annotations. To address these problems, I present a type system that combines, in a controlled way, first-order polymorphism with intersection types, union types and subtyping, and provide an algorithm to automatically reconstruct (infer) the type of functions. This results in a type discipline in which unannotated functions are given polymorphic types (thanks to Hindley-Milner) that can capture the overloaded behavior of the functions they type (thanks to intersection types) and that are deduced by applying advanced techniques of type narrowing (thanks to union types). This makes the system a prime candidate for typing dynamic languages.

Distributed systems are collections of processes that collaborate. They are behind many modern services, from online banking to social media. A central challenge in these systems is achieving consensus among all computers or processes. This challenge is addressed by agreement algorithms. They play an important role in ensuring the smooth operation of a distributed system. These algorithms help to ensure and maintain consistency and reliability across the system.

In this thesis, our primary focus was on the k-set agreement problem. This problem is a generalization of the conventional consensus problem, it centers on achieving an agreement among processes, where the agreement is on at most k values, with k=1 being the consensus. The task made complex when certain processes either crash or exhibit unpredictable behavior, known as Byzantine behavior. Our objective was to clarify the conditions under which the k-set agreement can be resolved and to delineate its solvability limits.

A key achievement of this research is the comprehensive mapping of the solvability of the k-set agreement. Through new and improved algorithms, we have boosted the efficiency of k-set agreement, especially in environments characterized by Byzantine behaviors and bounded message delays, encapsulated in the Byzantine synchronous message passing system, both in authenticated and unauthenticated environment.

Although our primary focus was the Byzantine synchronous message passing system, we also explored asynchronous environments characterized by the unpredictability of message deliveries and potential process crashes. Here, we extended the solutions to address these challenges, filling gaps left by prior studies.

To summarize, our study offers an exhaustive analysis on the k-set agreement within a Byzantine Synchronous message passing system, through innovative and optimal algorithms.

The capabilities of distributed systems in stochastic environments are inherently limited by the difficulty of efficiently circulating information. Additional limitations may arise whenever the entities making up these systems are competing against each others. To better understand these limitations, my thesis presents and analyses several idealised models, inspired by biological scenarios.

In this talk, I will present a counter-intuitive result that is reminiscent of Braess' paradox, albeit in the context of social foraging rather than network flows. Then, motivated by flocking scenarios, I will discuss the feasibility of alignment in the presence of drift noise. Finally, I will consider the self-stabilizing bit-dissemination problem, modelling the challenge of efficiently spreading information while reaching a consensus when communications are extremely constrained.

Overall, this presentation will aim to offer fresh insights into the capabilities of distributed and competitive biological systems, shedding new light on their potential and limitations.

To design efficient algorithms for combinatorial optimization, it is desirable, given a polytope, to find more compact formulations which are faster to handle, when they exist. Extension complexity of P is defined as the minimal size of an affine lift. In the nineties, Yannakakis characterized this complexity in terms of the slack matrix of the polytope. Slack matrices allow to derive upper bounds, when a succinct factorization is found (as for the regular n-gon in [FRT12]), or lower bounds, which can be deduced via a lower bound on the rectangle cover (correlation polytope, Kaibel and Weltge, 2014), or via more sophisticated techniques, as Fiorini's hyperplane separation lemma and entropy arguments à la Razborov (matching polytope, Rothvoss 2017). Faenza et al. (2011) gave an alternative characterization of extension complexity via certain randomised two-party protocols.

In this thesis, we propose a different model for randomised protocols, with a more flexible structure. The characterization still holds, and it additionally holds in the symmetric setting: there is a one-to-one correspondence between G-symmetric randomised protocols guessing P, and G-symmetric extensions of P. We also established an (affine) connection between two known extensions of the permutahedron (by Goemans and by Fiorini et al.), and by analogy we construct a simple extension of the regular n-gon, which turns out to be a section of the one obtained by factorization (in [FRT12]).

Two other independent works are presented in the thesis: in 2019, together with H. Fournier, G. Malod and S. Tavenas, we constructed a counter-example to a question asked by Nisan for monotone computations of non-commutative polynomials, via algebraic branching programs. Our construction also gave lower bounds for computing the elementary symmetric polynomials in the multilinear homogeneous setting. In 2018, C. Saroglou, I. Soprunov and A. Zvavitch have shown a characterization of the n-simplex as the only polytope minimizing a certain sup-ratio of mixed volumes related to the Fenchel inequality, and conjectured that the characterization holds among all convex bodies. I derived some necessary conditions on convex bodies to be minimizers, yielding a positive solution to this conjecture in R^3.

This manuscript is part of the field of formal verification, a computer science discipline aimed to ensure that programs are error-free. In this context, specification is one facet which consists of formally stating the properties the program has to satisfy. Our focus is on distributed algorithms which are particularly difficult to conceptualise. To tackle this problem, we explore data logic which is adapted to this purpose. In our framework, a data value is an element of a countable set, elements of structures have one or more data values and the logic can only test whether two data values are equal or not. The logics are analysed through the lens of the satisfiability problem. This work begins by exposing the state of the art concerning different logics on various structures such as words, multisets, data-words, data-multisets and graphs. Some identified gaps in the literature are filled, including missing proofs and unexplored cases. Additionally, two classical helpful tools in the analysis of the satisfiability problem are presented, namely Ehrenfeucht-Fraïssé games and domino problems. Afterwards, the main contribution of this work begins which is the definition and study of a new data logic, called the local fragment, introducing for this purpose the local modality. Inspired by the notion of locality and Gaifmans' graphs, our approach distinguishes itself by integrating locality in the definition of our logic, at the level of syntax. We show that our logic is indeed a fragment of first-order logic, as the local modality can be expressed in first-order logic. A sub-fragment called the existential fragment is also defined. Subsequently, our new logic from the point of view of the satisfiability problem is analysed; is identified criteria for which the logic is decidable and others for which it is not. Furthermore, in the cases where the logic is decidable, we try to analyse the complexity of the satisfiability problem, and succeeded in most of the cases.

Transducers are finite-state machines which compute functions (or relations) from words to words. They can be seen as simple programs with limited memory which manipulate strings. These machines have been studied for long in fundamental computer science as a part of automata theory, and are used in many areas such as compiling, natural language processing or stream processing.

Various transducer models have been defined in the literature, thanks to many features (such as non-determinism, two-wayness or nesting) which enable to increase the expressive power of the machines. In this setting, a natural question is to solve the related class membership problems: given a function computed by a transducer with “complex” features, can it be computed by a “simpler” transducer? Some of these problems have been solved in the literature, using somehow disparate proof techniques. They are generally considered as difficult. In practice, such problems can be interpreted as program optimization issues: given a program using a lot of resources, can we build a “more efficient” equivalent program?

This thesis solves various membership problems between existing classes of transductions, both over finite or infinite words. Among others, the celebrated models of two-way transducers and pebble transducers are investigated in detail. Each time, the membership procedure is non-trivial and turns out to be effective (in the sense that it builds a “simpler” transducer whenever it exists). Therefore our results can be considered as program optimization statements. Furthermore, we offer a systematic high-level strategy for solving these problems, which relies on semantic properties (i.e. dealing intrinsically with the functions) as well as syntactic properties (referring to the transducers which compute these functions).

Additionally, this thesis provides new computation models and characterizations in order to capture known classes of transductions. These results complete the previous understanding of these classes and provide new insights on their expressive power. The author believes that the various techniques of this manuscript form a rather extensive toolbox for investigating other open membership problems.

Preservation Theorems in first-order logic are a collection of results derived from classical Model Theory. These results establish a direct correspondence between the semantic properties of formulas and the syntactic constraints imposed on the language used to express them. However, studying these theorems becomes notably challenging when focusing on finite models, which is unfortunate given that the field of Finite Model Theory is better equipped to describe phenomena occurring in Computer Science. This thesis presents a systematic approach to investigating Preservation Theorems within the realm of Finite Model Theory. The traditional ad-hoc proofs are replaced with a theoretical framework that generalizes techniques based on locality, and introduces a topological presentation of preservation theorems called logically presented pre-spectral spaces. Introducing these topological spaces enables the development of a compositional theory for preservation theorems. Additionally, this thesis takes an initial stride towards systematically examining preservation theorems across inductively defined classes of finite structures. It accomplishes this by proving a generic fixed point theorem for a topological extension of logically presented pre-spectral spaces, specifically Noetherian spaces.

Details can be found here: https://www.irif.fr/~alopez/posts/2023-08-23.html

Temporal graphs are an extension of graphs which represent networks that evolve and change over time. In this context, the edges can be available at certain times and unavailable at others and they are called temporal edges. The length, or another property associated to an edge, that could classically be captured by the weight of an arc, can now have different values based on the time the edge is available. The classical notions from graph theory require novel definitions for temporal graph, taking into account the temporal dimension. A temporal walk, for instance, correspond to a sequence of adjacent temporal edges that are available one after the other. A node $v$ is temporally reachable from a node $u$ if there exists a temporal walk from $u$ to $v$. In this dissertation we explore problems that can be grouped into two main topics: temporal walk computation and temporalisation of a static graph.

We study the problem of computing minimum cost temporal walks, where ``cost'' is to be intended in a very wide sense. Indeed, we introduce an algebraic cost structure that can be instantiated to model all the classical criteria of walk optimisation in temporal graphs such as arrival time or duration, as well as linear combination of them or lexicographic compositions. Moreover, we study this problem in temporal graphs that are subject to waiting time constraints. Our main result on this topic is a temporal-edge scanning algorithm for single-source minimum-cost walks taking as input an acyclic time-expanded representation of the temporal graph and running in linear time. We also show that the setting in which we obtain linear-time is the widest possible: an additional logarithmic factor is needed both when the acyclicity assumption is dropped, or when a weaker temporal graph representation is used.

When we speak about temporalisation we are referring to the network design problem of turning a static graph into a temporal graph while optimising a certain criteria. In particular, we study a problem inspired by the optimisation of bus/metro/tramway schedules in a public transport network where each trajectory of a vehicle is modelled by a walk in the directed graph representing the map of the network. We consider the problem of turning a collection of such walks (called trips) in a directed graph into a temporal graph by assigning a starting time to each trip so as to maximise the reachability among pairs of nodes. We obtain several complexity results. Among them, we show that maximising reachability via trip temporalisation is hard to approximate within a factor $\sqrt{n}/12$ in an $n$-vertex digraph, even if we assume that for each pair of nodes, there exists a trip temporalisation connecting them. On the positive side, we show that there must exist a trip temporalisation connecting a constant fraction of all pairs if we additionally assume symmetry, that is, when the collection of trips to be scheduled is such that, for each trip, there is a symmetric trip visiting the same nodes in reverse order. Notice that symmetry is a fair assumption in the context of public transit networks, where a bus or metro line usually consists in trips in both directions.

The definition of algebraic structures on arbitrary types in homotopy type theory (HoTT) has proven elusive so far. This is due to types being spaces instead of plain sets in general, and equalities of elements of a type behaving like homotopies. Equational laws of algebraic structures must therefore be stated coherently. However, in set-based mathematics, the presentation of this coherence data relies on set-level algebraic structures such as operads or presheaves which are thus not subject to additional coherence conditions. Replicating this approach in HoTT leads to a situation of circular dependency as these structures must be defined coherently from the beginning.

In this thesis, we break this situation of circular dependency by extending type theory with a universe of cartesian polynomial monads which, crucially, satisfy their laws definitionally. This extension permits the presentation of types and their higher structures as opetopic types which are infinite collections of cells whose geometry is described by opetopes. Opetopes are geometric shapes originally introduced by Baez and Dolan in order to give a definition of n-categories. The constructors under which our universe of cartesian polynomial monads is closed allow us to define, in particular, the Baez-Dolan slice construction on which is based our definition of opetopic type.

Opetopic types then enable us to define coherent higher algebraic structures, among which infinity-groupoids and (infinity, 1)-categories. Crucially, their higher structure is univalent in that it coincides with the one induced by their identity types. We then establish some expected results in order to motivate our definitions.

In this thesis, we focus on the syndrome decoding problem (SDP), its generalization, cryptanalysis, and its application to digital signature scheme designs. We introduce a new problem, which we refer to as the generalized syndrome decoding problem. In the cryptanalytic part of the thesis, we then focus on the classical and quantum cryptanalysis of the generalized syndrome decoding problem using the information set decoding framework. More precisely, we calculate the running time of three different (classical) information set decoding algorithms, which we refer to as Prange's, Stern's/Dumer's, and Wagner's algorithms. The three algorithms are adapted to solve specific versions of the generalized problem which are given over the Hamming weight, taken as a baseline, and the Lee weight, taken as an alternative to the most commonly used Hamming weight. We then compare the obtained running times with the running time of the hybrid classical-quantum algorithm, obtained by introducing the Grover search and the amplitude amplification in the appropriate step of Wagner's algorithm. In the protocol design part of the paper, we modify Stern's identification protocol, and the corresponding signature scheme, to the newly introduced generalized syndrome decoding problem. To keep the zero-knowledge property of the scheme, we eventually replace the syndrome decoding problem with the permuted kernel one (PKP), for which we show that the average-case SDP reduces to average-case PKP. We then suggest different methods for optimizing the efficiency of the scheme and then provide numerical results that compare the efficiency of the original construction and our newly introduced scheme. The outcome of this work is an analysis of the newly introduced variant of the syndrome decoding problem that estimates the asymptotic complexity of the problem, as well as the concrete security of the scheme based on this problem. The results indicate that the proper choice of a weight function introduces a harder version of the syndrome decoding problem and thus yields more efficient protocols based upon it.

Graph partition is one of the central problem in graph theory, originated from the famous 4-color problem. In this thesis, two major problems concerning graph partition are considered: the edge separation of signed graphs and the vertex decomposition of sparse graphs.

In the first part of this thesis, we focus on signature packing problems of signed graphs. A signed graph $(G, \sigma)$ is a graph $G$ equipped with a signature $\sigma$ which assigns to each edge of $G$ a sign (either $+$ or $-$). The key concept that separates a signed graph from a 2-edge-colored graph is the notion of switching, a switching at a subset $X$ of vertices of $G$ is to multiply the signs of all edges in the edge-cut $(X, V\setminus X)$ by $-$. A signed graph $(G, \sigma')$ is said to be switching-equivalent (or simply equivalent) to $(G, \sigma)$ if it is obtained by a switching on an edge-cut. Then we define the signature packing number of a signed graph $(G, \sigma)$, denoted $\rho(G, \sigma)$, to be the maximum number of signatures $\sigma_1, \sigma_2,\cdots, \sigma_l$ such that each $\sigma_i$ is switching equivalent to $\sigma$ and the sets $E^{-}_{\sigma_i}$, negative edges of $(G,\sigma_i)$, are pairwise disjoint. We show that it is captured by specific homomorphism. Then we establish connection to several well-known problems: e.g. the four coloring problem, Seymour's edge coloring conjecture. More precisely, we first show that if $G$ is a $K_5$-minor-free bipartite simple graph, then for any signature $\sigma$ we have $\rho(G,\sigma)\geq 4$. Secondly, we continue using the language of packing number and extend the technique to verify that for any antibalanced signed planar graph $(G,\sigma)$ of negative girth at least $5$, $\rho(G,\sigma)\geq 5$. Thirdly, we study a generalization of the packing number. Instead of considering one signature and its equivalent signatures, we separate $k$ signatures which are not necessarily switching equivalent. Since there exists planar graph of packing number 1, we investigate sufficient conditions for a planar graph such that we could separate 2 or 3 signatures.

The second part of this thesis is about vertex decomposition of sparse graphs. We first study the vertex decomposition of planar graphs of girth at least $5$. It is known that every planar graph of girth at least $5$ can be vertex decomposed into two induced subgraphs, one of maximum degree at most 3, the other of maximum degree at most 5. We strengthen this result by showing that these induced subgraphs can be chosen to be forests. We then work on sparse graphs with maximum average degree condition. More precisely, we use potential method to prove that every graph $G$ of $mad(G)\leq \frac{16}{5}$ can be vertex decomposed into two forests of maximum degree at most 1 and 4. Consequently, every graph of genus at most $1$ and girth at least $6$ also admits such decomposition.

The principal goal of this thesis is to use the framework of polygraphs for a fine study of the shapes of higher-dimensional cells (of dimension 3, and implicitly of dimension 4) arising from quadratic normalisations appearing in combinatorial group theory. The thesis includes constructing coherent presentations of a class of monoids admitting a right-noetherian Garside family. Thereby, it presents a unifying generalisation of two distinct extensions of Deligne's original construction of coherent presentations of spherical Artin-Tits monoids, given by Gaussent, Guiraud and Malbos: to general Artin-Tits monoids, and to Garside monoids. In addition, a coherent presentation of monoids admitting quadratic normalisation of class (4, 3) is constructed and specialised to the already known column coherent presentation of plactic monoids of type A, constructed by Hage and Malbos. Furthermore, correspondences are established between the notion of quadratic normalisations (developed by mathematicians in France, led by Dehornoy) and the notion of factorability (developed by mathematicians in Germany led by Bödigheimer, with the goal of using suitable normal forms to understand group homology). Namely, factorable monoids are characterised in the axiomatic setting of quadratic normalisation. Additionally, quadratic normalisation of class (4,3) is characterised in terms of factorability and a condition ensuring the termination of the associated rewriting system.

Complexity measures of Boolean functions capture various aspects of the hardness of computing a function and their study is about finding connections between different complexity measures.

In the first part of this thesis, we introduce and study Certificate Game complexity, a measure of complexity based on the probability of winning a game in which two players are given inputs with different function values and are asked to output some index $i$ where their inputs differ, in a zero-communication setting. We give upper and lower bounds for private coin, public coin, shared entanglement and non-signaling strategies, and give some separations.

In the second part of this thesis, we revisit the celebrated proof of the sensitivity conjecture by Hao Huang. Using spectral techniques, Huang proved that every subgraph of the hypercube Hn of dimension n induced on more than half the vertices has maximum degree at least $\sqrt{n}$. Combined with earlier work, this completed a proof of the sensitivity conjecture. We show an alternate proof of Huang’s result using only linear dependency of vectors associated with the vertices of the hypercube. Our approach helps gain insight on more structural properties of the induced subgraph in addition to the largest degree. As an application, we show that for any Boolean function $f$, the polynomial degree is bounded above by the product of 0-sensitivity and 1-sensitivity, $s_0(f)s_1(f)$, a strictly stronger statement which implies Huang’s theorem. We also obtain structural relations for induced subgraphs at distance 3.

A key implement in Huang’s proof was signed hypercubes with the property that every cycle of length 4 is assigned a negative sign. We take a detailed look at this signature and give a nearly optimal signature that uses the minimum number of negative edges while ensuring that every 4-cycle is negative. This problem turns out to be related to one of Erdős’ problems on the largest 4-cycle free subgraph of the hypercube.

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.

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.

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

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.

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

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.

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

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

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

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.

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

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

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.

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

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

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.

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.

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

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

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

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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

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

This thesis explores the benefits of non-laziness in both Implicit Computational Complexity and probabilistic computation. More specifically, this thesis can be divided in two main parts. In the first one, we investigate in all directions the mechanisms of linear erasure and duplication, which lead us to the type assignment systems LEM (Linearly Exponential Multiplicative Type Assignment) and LAM (Linearly Additive Multiplicative Type Assignment). The former is able to express weaker versions of the exponential rules of Linear Logic, while the latter has weaker additive rules, called linear additives. These systems enjoy, respectively, a cubic cut-elimination and a linear normalization result. Since linear additives do not require a lazy evaluation to avoid the exponential blow up in normalization (unlike the standard additives), they can be employed to obtain an implicit characterization of the functions computable in probabilistic polynomial time that does not depend on the choice of the reduction strategy. This result is achieved in STA⊕, a system that extends STA (Soft Type Assignment) with a randomized formulation of linear additives. Also, this system is able to capture the complexity classes PP and BPP. The second part of the thesis is focused on the probabilistic λ-calculus endowed with an operational semantics based on the head reduction, i.e. a non-lazy call-by-name evaluation policy. We prove that probabilistic applicative bisimilarity is fully abstract with respect to context equivalence. This result witnesses the discriminating power of non-laziness, which allows to recover a perfect match between the two equivalences that was missing in the lazy setting. Moreover, we show that probabilistic applicative similarity is sound but not complete for the context preorder.

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.

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

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

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.

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

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.

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.

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.

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.

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

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.

http://www.normalesup.org/~cagne/soutenance.html

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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/

http://research.grellois.fr/phd.htm