Date: May 13, 2026
Place: A008
Chairs: Charlie Jacomme and Engel Lefaucheaux
Tentative Schedule
10h00-12h:
- Colin Blake, Equational Reasoning for Qudit Circuits (40 minutes)
- Clement Herouard, Secrecy in Squirrel and the Post-Compromise Security of a Ratchet (40 minutes)
- Tom Gouville, DDYF: Differential Dolev-Yao Fuzzing of Cryptographic Protocols (40 minutes)
12h00: pizzas in “salle club” (the room between the restaurant and the cafeteria)
13h00: coffee
13h30-15h35:
- Remi Pallen, Parameterized Complexity of Relations Between Subshifts (30 minutes)
- Florent Krasnopol, Graph-based Automated Theorem Proving for Quantum Circuit Equivalence (20 minutes)
- Kathleen Barsse, Classicality of quantum loops (35 minutes)
- Thomas Vinet, Resource-Aware Quantum Programming with General Recursion and Quantum Control (40 minutes)
Detailed program
Colin Blake: Equational Reasoning for Qudit Circuits
Abstract: Quantum programs are most often represented as quantum circuits: sequences of gates acting on registers of quantum systems. But in practice, writing a circuit is only the beginning. To optimise code, adapt it to hardware constraints (connectivity / mapping), and verify correctness, we need reliable ways to transform circuits while preserving their meaning. A convenient approach is equational reasoning: we specify a set of rewrite rules (axioms) and use them to derive when two circuits are equivalent.
My PhD focuses on extending this story beyond qubits, towards higher dimensions (qudits), and on making equational theories usable by reducing redundancy and organising rewrite systems around normal forms etc.
In this talk I will first introduce the basic ideas of quantum circuits and explain why gate sets and circuit fragments play an important role in quantum software. I will then discuss how equational reasoning is used to reason about and optimise circuits, and how these ideas extend to higher-dimensional quantum systems. Finally, I will present some of my recent work on equational theories for different kind of qudit circuits and explain how it fits into the broader goal of building practical tools for reasoning about quantum programs.
Clément Hérouard: Secrecy in Squirrel and the Post-Compromise Security of a Ratchet
Abstract: The Signal protocol is widely deployed in many secure messaging applications such as Signal Messenger, WhatsApp, and Apple’s iMessage PQ3. A core component of its security is the double ratchet, ensuring a strong security guarantee named Post-Compromise Security (PCS). It ensures message end-to-end encryption, even if the attacker can corrupt some specific keys. Until now, no mechanised cryptographic proof of PCS exists for a ratchet due to the complexity of the cryptographic arguments involved.
We tackle this problem with the Squirrel proof-assistant. The task is still a challenge because Squirrel’s indirect modeling of secrecy has difficulties in scaling to such a complex proof. To address these issues, we develop a novel logical framework that allows us to reason on secrecy as a first-class notion, and we validate our approach by verifying the PCS of an asymmetric ratchet. This provides the first mechanized computational proof of PCS to date for a ratchet, and possibly for any protocol.
Tom Gouville: DDYF: Differential Dolev-Yao Fuzzing of Cryptographic Protocols
Abstract:
Remi Pallen: Parameterized Complexity of Relations Between Subshifts
Abstract: Subshifts are sets of colorings. Several relations between subshifts are very commonly studied nowadays: equality, inclusion, being “dynamically equivalent” (i.e. conjugate), and many others. Their complexities are well known (often undecidable), and in this seminar we will discuss their parameterized complexities. For example, for a fixed subshift Y, what is the complexity of determining whether a subshift X is conjugate to Y? Understanding the complexity of these problems, and in particular identifying the boundary between decidability and undecidability, helps shed light on the deeper reasons behind the undecidability of their non-parameterized versions.
Florent Krasnopol: Graph-based Automated Theorem Proving for Quantum Circuit Equivalence
Abstract: Deciding the equivalence problem of quantum circuits is a major question, for which no efficient approach has already been found.
The strategy which consists in computing the semantics of both circuits and comparing them is practically inefficient, since it requires to compute complex matrices whose the size is exponential in the number of the circuits q-bits.
However, it is known that all equivalences between quantum circuits are captured by a finite set of equations.
Therefore, an other strategy is to use these equations as a fixed set of syntactic rewrite rules until both circuits become identical.
To develop such a method represents a challenge in between diagrammatic reasoning and computation over the real numbers, since one of these equations, Euler decomposition, involves a system of trigonometric equations.
On the negative side, real arithmetic with trigonometric functions and < is undecidable.
On the positive side, superposition, a technique that efficiently handles constrained equations, has recently been adapted by Echahed, Echenim, Mhalla and Peltier to handle equations where variables are graphs.
In this talk, I will present how the rooted and labelled graphs introduced by Echahed, Echenim, Mhalla and Peltier can be specified to represent faithfully (quantum) circuits, aiming at using the superposition calculus to derive equivalence on circuits.
Kathleen Barsse: Classicality of quantum loops
Abstract: In quantum computing, the execution flow of programs is generally based on classical information. Concretely, it is determined by primitives such as if-then-else statements and while loops, where the choice of the branch to be executed depends on a classical bit. To develop a fully quantum model, it is necessary to include quantum versions of these classical statements. In recent years, a variety of programming languages featuring quantum if-then-else statements have been developed. But the question of defining a quantum while loop is still often considered problematic. In this talk, I will discuss some of the difficulties involved with defining quantum while loops, and argue that a natural definition of quantum while turns out to be no more expressive than a classical while. We give a construction of quantum while loops based on existing definitions of quantum if-then-else statements, and give a denotational semantics for a minimal language with quantum loops. We show that the quantum semantics reduces to classical control.
Thomas Vinet: Resource-Aware Quantum Programming with General Recursion and Quantum Control
Abstract: This talk will discuss about the hybrid quantum language with general recursion Hyrql, driven towards resource-analysis.
By design, Hyrql does not require the specification of an initial set of quantum gates.
Hence, it is well amenable towards a generic cost analysis, unlike languages that use different sets of quantum gates, which yield quantum circuits of distinct complexity.
One perk of Hyrql is that we can relate the runtime of an expressive fragment of \hyrql programs with the size of the corresponding quantum circuits.
We also manage to capture the class of functions computable in quantum polynomial time, which, by Yao’s Theorem, corresponds to families of circuits of polynomial size.
Finally, we will discuss about how we can translate terms of Hyrql to Term Rewrite Systems, and how we can relate faithfully termination and runtime complexity of both worlds.
This allows us to use existing techniques to check the verification of such properties, and, altogether, to be able to automatize giving guarantees on size of quantum circuits.