Büchi's seminal 1962 paper established the decidability of the monadic second-order (MSO) theory of the structure (Nat; <), and in so doing brought to light the profound connections between mathematical logic and automata theory. This talk presents our recent results on the decidability of expansions (Nat; <, P1, …, Pd) for various unary predicates P1, …, Pd. We focus in particular on predicates of arithmetic origin, such as Pow-k (powers of k) and N-k (k-th powers). The following is a representative sample of the results yielded by our techniques, which combine automata theory, algebra, number theory, dynamical systems, and combinatorics:

- The MSO theory of (Nat; <, Pow-2, Pow-3) is decidable.

- The MSO theory of (Nat; <, Pow-2, Pow-3, Pow-6) is decidable.

- The MSO theory of (Nat; <, Pow-2, Pow-3, Pow-5) is decidable subject to Schanuel's conjecture.

- The MSO theory of (Nat; <, Squares, Pow-4) is decidable.

- The MSO theory of (Nat; <; Squares, Pow-2) is Turing-equivalent to the MSO theory of (Nat; <, S), where S is the unary predicate corresponding to the binary expansion of s = sqrt(2). As s is widely believed to be a weakly normal number, the corresponding MSO theory is in turn expected to be decidable.

The talk will give an overview of our techniques in general, and the automata theory and algebra that enable the above results in particular.

Dans ce premier exposé basé sur l’article « Univalence in simplicial sets » (https://arxiv.org/abs/1203.2553) je détaillerai la notion de « fibration universelle » qui en est l’ingrédient essentiel. J’examinerai en parallèle ce que devient une telle construction lorsqu’on remplace les ensembles simpliciaux par le cadre beaucoup plus simple des ensembles tout court.

Smart contracts are programs that run on an interpreter cobbled together from a massively distributed network of mutually untrusting computers. Unsurprisingly, the unruly nature of the underlying execution engine has a profound impact on the behavior of the interpreter and thus the semantics of smart contracts.

Caught once again by my incurable curiosity, I have set out to delineate precisely what set smart contracts aside in the realm of programming languages.

This talk reports on some early results, modeling the semantics of smart contracts in a type-theoretic and monadic framework. The objective of this work is to support formal reasoning at the protocol level (that is, starting from a specification free from programming error).

We shall strive to stay on track and in good taste: the presentation will not cover any financial aspect of smart contracts.

We study key agreement in the bounded-storage model, where the participants and the adversary can use an a priori fixed bounded amount of space, and receive a large stream of data. While key agreement is known to exist unconditionally in this model (Cachin and Maurer, Crypto'97), there are strong lower bounds on the space complexity of the participants, round complexity, and communication complexity that unconditional protocols can achieve.

In this work, we explore how a minimal use of cryptographic assumptions can help circumvent these lower bounds. We obtain several contributions:

- Assuming one-way functions, we construct a one-round key agreement in the bounded-storage model, with arbitrary polynomial space gap between the participants and the adversary, and communication slightly larger than the adversarial storage. Additionally, our protocol can achieve everlasting security using a second streaming round.

- In the other direction, we show that one-way functions are *necessary* for key agreement in the bounded-storage model with large space gaps. We further extend our results to the setting of *fully-streaming* adversaries, and to the setting of key agreement with multiple streaming rounds.

Our results rely on a combination of information-theoretic arguments and technical ingredients such as pseudorandom generators for space-bounded computation, and a tight characterization of the space efficiency of known reductions between standard Minicrypt primitives (from distributional one-way functions to pseudorandom functions), which might be of independent interest.

Joint work with Chris Brzuska, Geoffroy Couteau and Willy Quach

Like time in physics, computations can be reversible: the inverse of a deterministic computation is itself a valid computation, provided the program's state retains sufficient information to allow rollback. However, reversing a computation in distributed systems presents a challenge due to non-determinism. The inversion process must respect causality to maintain consistency. Syntactically, reversing a concurrent program requires tracking computation events in a way that preserves information during reductions, despite the absence of a global scheduler. From a denotational perspective, traditional models interpret concurrent programs as partial orders of configurations, where configurations consist of sets of computation events. Executing a computation involves removing the corresponding events from all configurations using set difference, while discarding incompatible configurations. In this talk, we introduce a generalization of these traditional models to accommodate reversibility, employing symmetric difference. This approach interprets reversible computation as a partial group action on sets of configurations.

The discrepancy of a sequence measures how quickly it approaches a uniform distribution. Given a natural number $d$, any collection of one-dimensional so-called low discrepancy sequences $\{S_i : 1 \le i \le d\}$ can be concatenated to create a $d$-dimensional hybrid sequence $(S_1, . . . , S_d)$. Since their introduction by Spanier in 1995, many connections between the discrepancy of a hybrid sequence and the discrepancy of its component sequences have been discovered. However, a proof that a hybrid sequence is capable of being low discrepancy has remained elusive. In this talk, an explicit connection between Diophantine approximation over function fields and two dimensional low discrepancy hybrid sequences is provided.

Specifically, it is shown that any counterexample to the so-called $t$-adic Littlewood Conjecture ($t$-LC) can be used to create a low discrepancy digital Kronecker-Van der Corput sequence. Such counterexamples to $t$-LC are known explicitly over a number of finite fields by, on the one hand, Adiceam, Nesharim and Lunnon, and on the other, by Garrett and the Robertson. All necessary concepts will be defined in the talk.

Reachability analysis is a powerful technique that can be used to verify that dynamic systems, such as autonomous cars, robots, or power grids, are robustly safe despite disturbances, measurement errors, and uncertain behavior of other agents in the environment. However, one substantial bottleneck of all state-of-the-art reachability algorithms is the necessity to adequately tune specific algorithm parameters, such as the time step size, which requires expert knowledge. This talk presents a new type of reachability algorithm, which already tunes all parameters internally until safety of the system with respect to unsafe sets or temporal logic specifications can either be proven or falsified. Our automated algorithm enables also non-experts to apply reachability analysis with ease, and we hope that this will facilitate a more widespread use of formal methods for dynamic systems in both research and industry in the future.

A framed polytope is the convex closure of a finite set of points in Euclidean space together with an ordered linear basis. An n-category is a category that is enriched in the category of (n-1)-categories. Although these concepts may initially appear to be distant peaks in the mathematical landscape, there exists a trail connecting them, blazed in the 90's by Kapranov and Voevodsky. We will traverse this path, widening and improving it as we address some of their conjectures along the way. If time permits, using a special embedding of the combinatorial simplex, we will connect this trail to the one ascending Mount Steenrod. This connection will enable us to express the combinatorics of cup-i products in convex geometric terms, dual to those introduced earlier in the talk to define the nerve of higher categories.