PhD Defence: Kostia Chardonnet

Jan 9 14:00 ₂₀₂₃

Abstract: In this thesis, we are interested in the development of a Curry-Howard correspondence for quantum computing, allowing to represent quantum types and quantum control-flow. In the standard model of Quantum Computation, a classical computer is linked to a quantum coprocessor. The classical computer can then send instructions to allocate, update, or read quantum registers. The programs executed by the coprocessor are represented by a quantum circuit: a sequence of instructions that applies unitary operations to the input quantum bits. While the model is universal, in the sense that it can represent any unitary operations, it stays limited: it lacks of proper representation of non-causal execution flow. Normally, to represent branching, one can use a type system featuring a coproduct, allowing for the choice between two possible executions, but quantum circuits only feature qubits and tensors thereof. On the other hand, types and strongly related to logic via the Curry-Howard correspondence which states that types of programs correspond to formulas and programs to proofs, while the program evaluation is matched with the proof simplification. While this correspondence has been extended to multiple setting in classical computer, it has yet to emerge in quantum computing.

To address those problems we follow two different approaches: the first one, through the development of a linear and reversible programming language, capturing a subset of quantum computing, along with a Curry-Howard correspondence with the logic µMALL. The language comes in two versions: one representing exactly complete, reversible functions while the other one can represent partial functions. Both version comes with an expressivity result: in the former, one can capture the whole class of Primitive Recursive Functions, while in the later any Turing Machine we show how to capture any Turing Machine. The second approach follows the development of token-based semantics, inspired by Girard's Geometry of Interaction, for graphical language for quantum computation. In this approach, a token-based semantics was given for the ZX-Calculus: a graphical language for quantum computation capable of representing any linear operators. We show how the token-based semantics matches the denotational one. We extend the ZX-Calculus with a coproduct and an explicit tensor in the development of the Many-Worlds Calculus. This new languages comes with a token-based semantics and an equational theory. We show how quantum control can be represented in this system. Finally, the programming language is modified to be able to realize pure quantum computation and the graphical language is then used as a denotational model for it.

Jury:

• Laurent REGNIER, Professeur, University Aix Marseille - Reviewer
• Emmanuel JEANDEL, Professeur, University of Lorraine - Reviewer
• Miriam BACKENS, Lecturer, University of Birmingham - Examiner
• Pierre CLAIRAMBAULT, Chargé de recherche CNRS, University Aix Marseille - Examiner
• Delia KESNER, Professeure, University Paris Cité - Examiner
• Claudia FAGGIAN, Chargée de recherche CNR, Université Paris Cité - Examiner
• Benoît VALIRON, Maître de Conférence, CentraleSupélec, University Paris-Saclay - PhD supervisor
• Alexis SAURIN, Chargé de recherche CNRS, University Paris Cité - PhD supervisor
• Pablo ARRIGHI, Professeur, University Paris-Saclay - PhD director