We present a framework for quantum computation, similar to Adiabatic Quantum Computation (AQC), that is based on the quantum Zeno effect. By performing randomised dephasing operations at intervals determined by a Poisson process, we are able to track the eigenspace associated to a particular eigenvalue. We derive a simple differential equation for the fidelity leading to general theorems bounding the time complexity of a whole class of algorithms. We also use eigenstate filtering to optimise the scaling of the complexity in the error tolerance $ε$. In many cases the bounds given by our general theorems are optimal, giving a time complexity of $O(1/Δ)$ with $Δ$ the minimum of the gap. This allows us to prove optimal results using very general features of problems, minimising the amount of problem-specific insight necessary. As two applications of our framework we obtain optimal scaling for the Grover problem (i.e. $O(N^{1/2})$ where $N$ is the database size) and the Quantum Linear System Problem (i.e. $O(κ \log(1/ε))$ where $κ$ is the condition number and $ε$ the error tolerance) by direct applications of our theorems.

Joint work with Joseph Cunningham.

We investigate the structure of graphs of twin-width at most 1 and uncover nice relations with several classical classes of hereditary graphs. An important finding is that they are permutation graphs and that their permutation diagrams and contraction sequences are closely related. We use these combinatorial tools to establish a recursive decomposition theorem for twin-width 1 graphs, and deduce a simple recognition algorithm running in linear time.

Joint work with Jungho Ahn, Noleen Köhler, Christophe Paul, Amadeus Reinald, and Sebastian Wiederrecht.

The goal is to explore the recently found interplay between integer partitions and the dynamics of the triangle map (a type of multi-dimensional continued fraction algorithm). (This is joint work with Baalbaki, Bonanno, Del Vigna and Isola.)

As we will see, the triangle map gives an almost internal symmetry from the set of integer partitions to itself, which in turn allows the generation of any number of new partition identities.

Further, this allows us to place a tree structure on the space of all integer partitions. (This is joint work with Joe Fox and with Jacob Lehmann Duke). This tree structure allowed us to find the natural extension of the triangle map in any dimension. As with the classical Farey map, the dynamics of this map, in every dimension, has an indifferent fixed point, which in turn can be used to understand the structure of the integer partition tree.

Among the many different types of multi-dimensional continued fractions that exist, for still unknown reasons it appears that the triangle map is the only one that is “partition” compatible.

Thus we use the triangle map (stemming from number theory and dynamics) to understand classical integer partition numbers from combinatorics, and use partition numbers to understand the dynamics of the triangle map.

The convertibility test, which checks if two λ-terms are equal up to β-reduction, is an essential part of typechecking and proof verification in proofs assistants based on type theory, such as Coq, Agda and Lean. Naturally, the correctness of such a test is necessary to ensure the proofs thus verified are valid; but having an efficient test is also required both for real-time interaction with the user, and for proof search.

In this presentation, we start with an efficient, strong call-by-need, big-step semantics for the λ-calculus, which is the critical building block to implement a convertibility test in a classical manner. We then show how we can improve upon this by considering the convertibility problem in its entirety, viewing it as proof search. To this end, we study what can be considered a (non-)convertibility proof, drawing upon existing work.

This gives rise to a new parallel, heuristic-less algorithm for this test, which does not duplicate computations, and comes with worst-case complexity guarantees. We derived a virtual machine from this algorithm, and made it more efficient by following Grégoire and Leroy, showing that our algorithm is suited to compilation of the input λ-terms for additional efficiency. Both this semantics and this efficient parallel convertibility test have been implemented in OCaml and experimentally validated, significantly outperforming Coq in some cases. They are also both formalised and verified using Coq, building confidence in our work.

Quantum protocols involve a number of features like concurrent execution, quantum primitives, message communication and non-determinism. The well-studied calculi and models for probabilistic concurrent systems seem inadequate in the quantum setting, as they do not comply with the observational limitations of quantum theory. We will explore a new semantic model made of “Quantum Distributions” and “Quantum Transition Systems”, instead of probability distributions and probabilistic LTSs. We provide a symbolic, quantum semantics for a minimal quantum process calculus, which we prove sound and complete with respect to the known ground, probabilistic behaviour of quantum processes.

In a paper of 1976, Rauzy studied two complexity notions, $\underline{β}$ and $\overline{β}$, for infinite sequences over a finite alphabet. The function $\underline{β}$ is maximum exactly in the Borel normal sequences and $\overline{β}$ is minimum exactly in the sequences that, when added to any Borel normal sequence, the result is also Borel normal. Although the definition of $\underline{β}$ and $\overline{β}$ do not involve finite-state automata, we establish some connections between them and the lower $\underline{\dim}$ and upper $\overline{\dim}$ finite-state dimension (or other equivalent notions like finite-state compression ratio, entropy or cumulative log-loss of finite-state predictors). We show tight lower and upper bounds on $\underline{\dim}$ and $\overline{\dim}$ as functions of $\underline{β}$ and $\overline{β}$, respectively. In particular this implies that sequences with $\overline{\dim}$ zero are exactly the ones that that, when added to any Borel normal sequence, the result is also Borel normal. We also show that the finite-state dimensions $\underline{\dim}$ and~$\overline{\dim}$ are essentially subadditive.

Together with Fixed Priority Scheduling, Earliest Deadline First (EDF) is the second leg on top of which a large portion of the research on real-time systems stands. At the heart of the EDF exact schedulability test, a pivotal role is played by the demand bound function test, which requires to evaluate whether the amount of work required to complete a set of jobs is less than or equal to the amount of time available. Such a test is checked over a set of time instants.

In this work, it is proposed a method that cuts drastically the set of constraints to be checked. Such a method is applicable also to tasks with release offset. Notably, it is proved that such a reduced set of constraints is minimal: it is not possible to reduce the set any further without losing the sufficiency of the test. The code to make this reduction is publicly available on GitHub.

Twenty-five years ago, Kaplan and Tarjan established a striking result: there exist “purely functional, real-time deques with catenation”. In other words, there exists a data structure that supports the following operations: “push” and “pop” which insert and extract one element at the front end, “inject” and “eject” which insert and extract one element at the rear end and “concat”, the concatenation operation. Moreover, the data structure is persistent: none of the five operations modifies or destroys its argument. Finally, each operation has worst-case time complexity O(1). This presentation will provide an overview of the first ever implementation of the data structure, done in OCaml, and its verification in Rocq.

Back in 1939, Frucht proved that every finite group is isomorphic to the automorphism group of a finite graph. This incited an examination of the influence that standard graph theoretical concepts can have on automorphism groups. Eventually, the framework was enlarged by extending the analyses to endomorphism monoids. This has ultimately established a particular connection between semigroup classes and graph classes, notably in terms of sparsity and combinatorial regularity. The goal of the presentation is to contextualize a new result on endomorphism monoids of regular graphs that adds some detail to the picture. This is joint work with Kolja Knauer.