See https://chocola.ens-lyon.fr/events/seminaire-2025-12-11/

Consider a data structure problem with possible data coming from a set D, queries coming from a set Q, and in the dynamic case updates coming from a set U. Then, the current state of the art in data structure lower bounds is t = \tilde\Omega(\log Q|) for static data structure problems, and max(t_q,t_u) = \tilde\Omega(log^2 n) where n = max(|Q|,|U|,log |D|) for dynamic.

We port Razborov and Rudich's natural-proofs framework to the setting of static and dynamic data structures in the cell probe model, in a way that strongly suggests this state of the art is unlikely to be improved anytime soon. A similar direction was recently taken also by Korten, Pitassi and Impagliazzo (FOCS 2025) who look at static data structure lower bounds in a different regime of parameters. Our contribution is:

- We define notions analogous to pseudorandom functions (PRF). We call these primitives *local PRFs*, in the context of static data structures, and *local and locally updatable (LLU) PRFs*, in the context of dynamic data structures.

- We then formulate cryptographic conjectures, namely, that secure local PRFs and secure LLU PRFs exist, precisely at the frontier where we are no longer able to prove static, respectively dynamic, data structure lower bounds. If these conjectures are true, it follows that the current state of the art in data structure lower bounds cannot be improved by a natural proof.

- We show that (almost) every single known data structure lower bound proof is a natural proof, by surveying all lower bounds in the literature (known to us). (The only exception is proofs based on lifting theorems.)

- It follows that, if our cryptographic conjecture is true, then all known lower bound proof techniques (minus the two exceptions) are unable to improve upon the state of the art. (We also present obstacles for the two exceptions.)

- Further, we provide concrete candidate constructions for our two pseudo-random primitives. We conjecture that our constructions are secure for parameters just above the state-of-the-art lower bounds.

- We also show that, whether or not they are secure, our candidate PRFs at least satisfy the natural properties appearing in all (but one) known proofs.

- So if one is interested in improving upon the state of the art in static or dynamic data structure lower bounds, one must either find a non-natural method of proving such lower bounds (no such method currently exists), or one may as well begin by trying to break our PRF candidates.

Significant progress has been recently achieved in developing efficient solutions for simple stochastic games (SSGs), focusing on reachability objectives. While reductions from stochastic parity games (SPGs) to SSGs have been presented in the literature through the use of multiple intermediate game models, a direct and simple reduction has been notably absent. We introduce a novel and direct polynomial-time reduction from quantitative SPGs to quantitative SSGs. By leveraging a gadget-based transformation that effectively removes the priority function, we construct an SSG that simulates the behavior of a given SPG. We formally establish the correctness of our direct reduction.

This work was presented at CONCUR 2025.

Cangjie is a high-level, statically typed, general-purpose, multi-paradigm, compiled imperative and declarative programming language developed by Huawei. It was first released on June 21, 2024, as part of developer beta recruitment, for HarmonyOS NEXT app development on the preview version of the HarmonyOS operating system. It is also referred to as CangjieLang or CJ, but its proper name is Cangjie.

Reference: https://cangjie-lang.cn/en/docs

This talk investigates the structure and role of universes in the formalisation of higher categorical structures, towards a formalisation of the hierarchy of the (very large) n+1-category of n-categories. The focus is on motivations and conceptual aspects of ongoing work. I will review notions of smallness in higher categorical structures, bringing together perspectives from homotopy type theory and more classical categorical intuitions. I will then discuss how truncation hierarchies – such as n-truncated types and n-categories – interact with universes under univalence, and use it to outline connections between HoTT and the framework I am developing.

Given a connected graph G = (V, E) where V is known and E is hidden, we are provided access to an oracle that can answer the following queries: given u, v in V, the oracle returns the distance of the shortest path between u and v in G. This setup naturally arises in network recovery and phylogenetic reconstruction problems. This talk explores what is known about the query complexity for various classes of graphs and recent developments toward the main open conjecture in the area: is it possible to reconstruct graphs of bounded degree using n*polylog(n) queries, where n denotes the size of V? This talk is based on joint work with Carla Groenland.

Consider a simple (to formulate…) mathematical object: you are given a finite collection of matrices $A_i\in GL(2,\mathbb R); i=1,\ldots,k$ and you are allowed to multiply them, in any order. The notion you are interested in is the exponential rate of speed of growth of the norm: given $\omega\in \{1,\ldots,k\}^{\mathbb N}$, let \[ \lambda(\omega) = \lim_{n\to\infty} \frac 1n \log ||A_{\omega_n} \cdot \ldots \cdot A_{\omega_1}||. \] This object has many names, in dynamical systems we call it the Lyapunov exponent.

We are in particular interested in the set of those $\omega$'s that give the extremal (maximal, minimal) value of the Lyapunov exponent. A long-standing conjecture states that for a generic matrix collection those sets ought to be {\it small}, in some sense. In the result I will present we (Jairo Bochi and me) are proving that for certain open set of collections of matrices those $\omega$'s that maximize/minimize Lyapunov exponent have zero topological entropy.

Modern applications are centered around using large-scale distributed storage systems for storing and retrieving data. Storage systems provide different levels of consistency that correspond to different trade-offs between consistency and throughput. The weaker the consistency is, the more behaviors the storage is allowed to exhibit. In this thesis we address the problem of specifying and verifying a (distributed) storage system with respect to a given consistency model from three different perspectives.

The first problem we focus is studying the correctness of applications using database and isolation levels – database consistency models. We propose Stateless Model Checking algorithms that rely on Dynamic Partial Order Reduction. These algorithms work for a number of widely-used weak isolation levels, including Read Committed, Causal Consistency, Snapshot Isolation and Serializability. We show that they are complete, sound and optimal, and run with polynomial memory consumption in all cases. We report on an implementation of these algorithms in the context of Java Pathfinder applied to a number of challenging applications drawn from the literature of distributed databases.

The second question we focus on is the problem of testing isolation level implementations in databases, particularly when databases are accessed by transactions formed of SQL queries using multiple isolation levels at the same time. We show that many restrictions of this problem are NP-complete and provide an algorithm which is exponential-time in the worst-case, polynomial-time in relevant cases, and practically efficient.

The third problem we study is the ability of distributed storage systems to remain available even in the presence of network failures with respect to the consistency guarantees they provide. The CAP theorem states that a distributed storage system cannot deliver both availability and strong consistency, in the presence of network partitions. We present a more precise classification of distributed storage systems, conditioned on the combination of their consistency guarantees and the data type semantics they support, which can be implemented in a highly-available manner. The characterization reveals that the key to availability is the ability to locally determine responses without having to arbitrate between several possible dependencies. The results apply to a wide set of consistency models, including Causal Consistency, Sequential Consistency and Delayed Consistency, and to a large collection of objects including counters, Last-Writer-Wins and Multi-Value Key-Value stores, or transactional and non-transactional SQL.