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.

We study the quantum security of key-alternating ciphers (KAC), a natural multi-round generalization of the Even–Mansour (EM) construction. KAC abstracts the round structure of practical block ciphers (e.g. AES) as public permutations interleaved with key XORs. The 1-round KAC or EM setting already highlights the power of quantum superposition access: EM is secure against classical and Q1 adversaries (quantum access to the public permutation), but insecure in the Q2 model (quantum access to both the permutation and the cipher). The security of multi-round KACs remain largely unexplored; in particular, whether the quantum-classical separation extends beyond a single round had remained open.

Quantum Lower Bounds. We prove security of the t-round KAC against a non-adaptive adversary in both the Q1 and Q2 models. In the Q1 model, any distinguisher requires \Omega(2^{tn/(2t+1)}) oracle queries to distinguish the cipher from a random permutation, whereas classically any distinguisher needs \Omega(2^{tn/(t+1)}) queries. As a corollary, we obtain a Q2 lower bound of \Omega (2^{(t-1)n/2t}) quantum queries. Thus, for t>=2, the exponential Q1-Q2 gap collapses in the non-adaptive setting, partially resolving an open problem posed by Kuwakado and Morii (2012). Our proofs develop a controlled-reprogramming framework within a quantum hybrid argument, sidestepping the lack of quantum recording techniques for permutation-based ciphers; we expect this framework to be useful for analyzing other post-quantum symmetric primitives.

Quantum Key-Recovery Attack. We give the first non-trivial quantum key-recovery algorithm for t-round KAC in the Q1 model. It makes O(2^{t(t+1)/((t+1)^2 + 1)}) queries, improving the best known classical bound of O(2^{tn/(t+1)}). The algorithm adapts quantum walk techniques to the KAC structure.

Learning temporal properties has crystallized as an effective mean to explain complex temporal behaviors. Thus, we study the problem of learning (passively) temporal logic formulas from (positive and negative) examples of system behavior. The goal of this talk is to explore various aspects of this problem, including its complexity, and the different methods used to solve it (constraint-solving, enumerative search, neuro-symbolic). We will also briefly examine a variant of this problem, where the goal is to learn DFAs from positive examples only.

This talk is based on my work during my previous Post-Doc at TU Dortmund.

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.

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.