Time complexity and message complexity (or communication cost) are two fundamental performance measures of distributed algorithms. Time complexity has been extensively studied, and efficient distributed algorithms with optimal or near-optimal time complexities have been developed over the last two decades for fundamental graph optimization problems such as diameter, all-pairs shortest paths (APSP), maximum matching (MaxM), minimum dominating set (MDS) and more. On the other hand, the communication cost of these fundamental problems has remained largely unknown.

In recent results, we significantly improve our understanding of the communication cost of distributed algorithms. First, we give cubic message complexity lower bounds for some graph optimization problems (such as MDS), and these cubic message complexity lower bounds are the first of their kind. Second, we provide the first message-optimal distributed algorithms for diameter and APSP. However, these algorithms are not time-optimal (whereas the prior known time-optimal algorithms were message-inefficient). Following which, we show that between the time-optimal (but message-inefficient) and message-optimal (but time-inefficient) algorithms for diameter and APSP, there exists in fact a natural, smooth time-message trade-off.

My research focuses on formally proving programs efficient. Parallelism is a natural path to time-efficiency, but it often turns clarity into chaos: memory management management becomes tricky when multiple tasks access shared resources, and formal verification is harder because every possible interleaving must be verified. This talk presents two contributions I developed during my postdoc to address these challenges. Both works were conditionally accepted at POPL'26 and are mechanized in Rocq using the Iris Separation Logic framework.

In the first part, I will introduce TypeDis, the first type system for disentanglement. Disentanglement is a property ensuring that parallel tasks remain oblivious to each other's allocations; such a restriction is key to efficient automatic memory management. Inspired by region types, TypeDis annotates each type with a timestamp identifying its allocating task. It supports recursive types and allows polymorphism over types and timestamps. Crucially, timestamps are allowed to change during type-checking via a form of subtyping, dubbed subtiming.

In the second part, I will present schedule-independent safety, a property allowing deterministic parallel programs to be verified as if they were sequential. I will describe automatic ways to enforce this property and a program logic that allows the user to cherry-pick an interleaving to verify. We illustrate schedule-independent safety with several examples that make use of shared memory in a deterministic way.

Let $S$ be an iterated function system with full support. Under some restrictions on the allowable rotations, we will show that $S$ satisfies the weak separation condition if and only if it satisfies the generalized finite-type condition. To do this, we will extend the notion of net intervals from $\mathbb{R}$ to $\mathbb{R}^d$. If time allows, we will also use net intervals to calculate the local dimension of a self-similar measure with the finite-type condition and full support. This talk is based on joint work with Kevin G. Hare.

Working with weighted automata naturally leads to the problem of the definition of the (Kleene) star operation on the semiring of (formal power) series. In contrast with the case of languages, the star of a series is not always defined, as the star is not always defined in the weight semiring. The identity:

(s_0 + s_p)* = (s_0)* (s_p (s_0)*)*

where s_0 and s_p are respectively the 'constant term' and the 'proper part' of a series s, is central in this theory, both for characterising the series whose star is defined and for proving that rational series are realised by weighted finite automata (one direction of Kleene–Schützenberger Theorem).

In my book 'Elements of Automata Theory', a proof of the above identity was given under the hypothesis that the weight semiring has the property that the product of two summable families is a summable family. Such semirings were called 'strong' and even though all known semirings were strong, the conjecture was stated that there should exist some semirings which are not strong.

In this talk, and after setting the framework of the topological approach to the definition of star and recalling the proof of the quoted theorem, we present a construction that provides an example of a semiring — indeed, a ring — which is not strong.

Joint work with David Madore (LTCI, Télécom Paris)

Discrete optimization problems in graphs range from shortest paths (used e.g. for finding a point-to-point route) and maximum flow through network design (select arcs to comprise a network, e.g. for communication or heating) to the traveling salesperson problem and vehicle routing problem.

In our pursuit of efficient and accurate algorithms for optimization problems in graphs, we encounter some apparently fundamental obstacles. For certain polynomial-time problems, there seem to be limits to how fast we can solve them in the worst case. For certain NP-hard problems, there seem to be limits on how accurately we can approximate them.

One way to overcome these limits is to restrict the input. It turns out that requiring the input graph be planar (e.g. the graph can be drawn on the plane such that no edges cross) allows us to break through the barriers: - for some problems, faster algorithms exist when the input is required to be planar than are known to exist when the input is unrestricted. - for some problems, more accurate approximation algorithms exist when the input is required to be planar than are believed to exist when the input is unrestricted.

We survey some of these algorithmic results, and discuss some potential applications. We finish by mentioning some ongoing work on implementation of some approximation algorithms on a parallel architecture, the GPU.

Some work is joint with Claire Mathieu and Glencora Borradaile.