I will introduce some consensus protocols and give an overview of some of the implementations. Following that, I will introduce what are the existing approaches to testing the implementations and then explain our approach which is akin to unit testing.

No prior knowledge of distributed systems/algorithms is required.

I will give an introduction to first order logic and proof theory in order to present a proof-search algorithm called “Method of analytic tableaux”. I will take this opportunity to talk about nice properties of proof theory and sequent calculus. The talk is more or less a lecture of the book “Introduction à la logique : Théorie de la démonstration” from David, Nour and Raffalli. It will not be about research I am currently working on and therefore should be more accessible to everyone. Looking forward to see you there!

Everything you always wanted to know (but were afraid to ask): What is it? Why should we care? How do we deal with it? No prior knowledge of quantum computing is required.

The Curry-Howard correspondence is a very well-known result among (theoretical) computer scientists. However, the link it establishes between programs and proofs has also been extended by Lambek to a certain class of categories. As such, from the perspective that category theory provides a foundational framework for reasoning and logic, it is interesting to identify the underlying categorical structure of models of a given type theory. While the connection is fairly well-understood for intensional flavor of type theory following the work of Hofmann, it is notable that the extension to homotopy type theory is more recent and still incomplete. The goal of this talk is to introduce the basic concepts of the so-called categorical semantic of type theory and its challenging homotopy counterpart.

The agreement problems has been extensively studied in distributed computing. Beyond the practical interest of this problem, particularly regarding fault-tolerant distributed computing, one of the main reasons behind the focus on agreement problem is the fact that it can be used to define and compare computational power properties of systems. In this presentation I will introduce two agreement problems: Byzantine General problem and k-set Agreement. In k-set agreement, each process must decide on value such that no more than k different values are decided by processes. In addition, the processes must guarantee a validity condition according to the failure models of the processes. Therefore, with crash process failures, the validity condition ensures that the decided values are initial values proposed by processes. In the case where k=1, the k-set agreement is the very classical consensus problem which is fundamental for fault tolerant distributed algorithms.

This will be an introductory session where we invite all (new and old!) non-permanent members to come and talk about their research interests. Each talk should be 2-5 minutes long, and understandable by everyone.

Imagine you are high-dimensional being with scissors that can make d-dimensional cuts into (d+1)-dimensional objects. How many regions can you split an object into with a fixed number of cuts? What if all of your cuts must pass through the center of the object? Are there special patterns of cuts with nice properties? We will study these questions and more through a brief introduction to hyperplane arrangements. Hyperplane arrangements are of much interest to combinatorialists, and as they encode the structure of many important combinatorial problems. We will also briefly discuss how hyperplane arrangements have played a fundamental role in the understanding of certain neural networks.

In the study of programming languages, an essential point is the ability to state program equivalence, whether it is to reason abstractly or to establish that some program transformations, used typically when compiling programs, preserve the behavior of programs. The topic of this talk is the study of program equivalence for the case of programs expressed as terms of the λ-calculus, seen as a mathematical model of functional programming languages. We will survey existing program equivalences and focus on normal form bisimulations, in different variants of the lambda calculus. The lambda calculus was first introduced as a way to represent computable functions, with the Call-by-Name variant which has been extensively studied. Nowadays, functional programming languages use mostly the Call-by-Value variant (OCamL) and some the Call-by-Need variant (Haskell). In Call-by-Name, normal form bisimulations yield very satisfactory results. Unfortunately, these do not export to Call-by-Value. Part of my thesis work will be trying to find a satisfactory program equivalence in Call-by-Value.

The previous talk by Victor Arrial is a nice introduction to this talk but concepts tied to the lambda calculus (and its variants) will be re-explained. We will also need the (more generic) concept of co-induction to form program equivalences, which will be briefly explained as well.

This talk is planned to be an informal (very much non-exhaustive) introduction to lambda calculus (from a syntactical point of view). The idea is to give intuition on the calculus and two different reduction strategies (Call-by-Value and Call-by-Name). We will then briefly explore/compare three typing systems (simple types, graded linear types, multitypes). It is intended as an introduction to a forthcoming talk on “Quantitative Inhabitation in Call-by-Push-Value” (non-permanents seminar).

The talk will be a 1-hour introductory session on category theory accessible to everyone. We introduce categories as generalizations of ordered sets and then focus on the notion of universal property and show through examples how such properties can be used to describe behaviours in different areas of mathematics in a unified way. No prerequisites.

In this talk, we will talk about the Data Stream Model of computation. In this model, the input arrives as a stream of items and the workspace of the algorithm is very low and therefore, the whole input cannot be stored in the memory. Due to space constraints, data streaming algorithms use elegant and non trivial randomization techniques to store summary of the input seen so far. The model is inspired by the advent of data explosion, where it is impossible to store all of the data in the memory and also by database applications, where random access cost is high. We will see algorithms for frequency moments computation ($F_0$ and $F_2$) over a stream of elements, which actually kickstarted the field of data stream algorithms. This talk is based on lecture notes from the course “Communication Complexity (for Algorithm Designers)” by Tim Roughgarden (http://timroughgarden.org/notes.html).

We begin by introducing Sturmian words, which are infinite words on a two letter alphabet. An infinite word ω is said to be Sturmain if, for any given n, there exist exactly n+1 distinct subwords of ω of length n. They are, in some sense, the simplest possible non-trivial words. Geometrically, they correspond to a cutting sequence obtained from a line of irrational slope on a square grid, and there is a very nice correspondence between the coding sequence of ω and the continued fraction expansion of the slope. Given N ≥ 1 and x ∈ [0, 1] \ Q, an N-continued fraction expansion of x is defined analogously as the classical continued fraction, but with the numerators being all equal to N. An infinite word ω(x, N) on a two letter alphabet is obtained as a limit word of a sequence of substitutions, which we call an NCF word. When N = 1, we find a Sturmian word. We present some combinatorial and analytic results obtained for NCF words, namely: balance properties, letter frequency, factor complexity. This is joint work with Niels Langeveld and Jörg Thuswaldner.

The longest common substring problem (LCS) is one of the most fundamental string problems. We look at the decision version of LCS: given two texts s and t and a parameter d we want to find out if there is a string of length d that appears as a substring in both s and t. Its classical complexity is well understood: it is linear in the length of s and t, which we denote by n. In the quantum setting, two algorithms can be combined to get the best known upper bound: one has query (and time) complexity O(n^(2/3)) for any value of d; and the other one uses O(n/sqrt(d)) queries. In the talk I will try to present the main ideas behind these results in such a way that people without much knowledge on quantum computing can follow too.

HA^ω (Higher Type Arithmetic) is a first order many sorted theory. It is a conservative extension of HA (Heyting Arithmetic a.k.a the intuitionistic version of Peano Arithmetic) obtained by extending the syntax of terms to all the System T : the objects of interest here are the functionals of “higher types”. While equality between natural numbers is well understood (it is canonical and decidable), how equality between functionals can be defined ? From this question, different versions of HA^ω arise : an extensional version (E-HA^ω) and an intentional version (I-HA^ω).

Picture a networked system of autonomous agents, each starting with some initial value. In the /average consensus/ problem, the agents should collectively compute the arithmetic mean of those values, through local interactions over a connected network.

Classically, this problem is considered in a setting where the agents hold no unique identifier, and do not start knowing a bound over the size of the system. These restrictive assumptions give rise to two major obstacles to our problem. First, it is generally impossible for an agent to detect that it has reached the desired answer; as such, we only expect the system to asymptotically converge towards the average, rather than to irrevocably decide on it. Second, it is generally impossible to properly account for the multiplicities of the initial values; we therefore restrict our considerations to bidirectional communication links.

For fixed bidirectional networks, an efficient solution is to be found in the /Metropolis/ averaging algorithm, first proposed by Xiao and colleagues in 2005. However, when moving to consider /dynamic/ networks – i.e., where the communication links can arbitrarily change at each step of the execution – the Metropolis rule isn't algorithmic, in the sense that it requires the agents cannot themselves gather all the information required to implement the rule. Other average consensus protocols proposed in the literature fare no better for the same reasons.

We propose the /MaxMetropolis/ rule, an adaptation of the Metropolis rule that is history-dependent, and admits a totally decentralized and local implementation. Over bidirectional dynamic networks with $n$ agents and connectivity delay $B$, $O(B n^4 log n/r)$ communication rounds are required to achieve a relative disagreement of $r > 0$ over the value of the average. This is the first truly distributed average consensus algorithm for bidirectional dynamic networks.

How to efficiently and reliably spread information in a system is one of the most fundamental problems in distributed computing as well as in the animal world. In this talk, we will consider the self-stabilizing bit-dissemination problem, motivated by biological scenarios, in the extremely constrained model of passive communication.

In a temporal graph, each edge appears and can be traversed at specific points in time. In such a graph, temporal reachability of one node from another is naturally captured by the existence of a temporal path where edges appear in chronological order. Inspired by the optimisation of bus/metro/tramway schedules in a public transport network, we consider the problem of turning a collection of 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. Each trip represents the trajectory of a vehicle and its edges must be scheduled one right after another. Setting a starting time to the trip thus forces the appearing time of all its edges. We call such a starting time assignment a trip temporalisation.

We will speak about results on the complexity of maximising reachability via trip temporalisation. We will show that the problem is hard to approximate even when we assume the nice property 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 in the trip network.

Finitely generated groups of matrices are fundamental mathematical objects that appear in a wide variety of areas in computer science, including algebraic complexity theory, quantum computation, dynamical systems, graph theory, control theory, and program verification. Unfortunately, matrix groups are challenging from the algorithmic point of view, with many natural problems being undecidable. In order to get a better handle on a finitely generated matrix group, it turns out to be worth over-approximating it by its Zariski closure, which admits a finite representation.

This talk will be a gentle introduction to (computing) the Zariski closure of finitely generated matrix groups with examples of applications in automata theory and program verification. We will describe an existing algorithm for computing the closure due to Derksen, Jeandel and Koiran. We will conclude by discussing our result, which is to obtain an upper bound on the degree of the polynomials that define the Zariski closure. Having an a priori bound allows us to give a simple algorithm for the problem, via linear algebra, similar to Karr's algorithm for obtaining affine invariants for affine programs.