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