Henri De Boutray : " Computational studies of quantum entanglement and contextuality with a view to their formal verification"

Abstract : Although current quantum computers are limited to the use of a few quantum bits, the foundations of quantum programing have been growing over the last 20 years. These foundations have been theorized as early as in the 80's but the complexity of their implementation caused these leads to be out of reach until very recently. In this context, the objective of this thesis is to contribute to the adaptation of the methods of formal specification and deductive verification of classical programs to quantum programs. I thus present my contributions to the study of quantum properties with the end goal of formalizing them. I study in particular quantum entanglement and quantum contextuality. These properties allow to classify quantum states and protocols, and in particular to differentiate them from classical ones. My study of entanglement is based more specifically on the evolution of entanglement during two quantum algorithms: the Grover algorithm and the Quantum Fourier Transform. To quantify entanglement along those algorithms, I use Mermin's polynomials, which have the advantage of being implementable in actual quantum computers. My study of contextuality, on the other hand, relies on finite geometries representing experiments, which are said to be contextual when no non-contextual classical theory can predict the results. These geometries are associated with the binary symplectic polar spaces. We study their structure, and eventually use this structure to get insights on quantum protocols using contextuality. The study of these properties led to interesting conjectures which we started to formalize in proof environments, such as Coq and Why3, but are left as perspective as these works have not reach a conclusion yet

Jury Composition :

M. Alain GIORGETTI Maître de recherche Université Bourgogne Franche-Comté PhD Director
M. Peter LÉVAY Maître de conférences Université de Technologie et d’Economie de Budapest Reporter
M. Jean-Gabriel LUQUE Professeur Université de Rouen Reporter
Mme Natacha PORTIER Maîtresse de conférences École Normale Supérieure de Lyon Reviewer
M. Emmanuel JEANDEL Professeur Université de Lorraine Reviewer
M. Christophe GUYEUX Professeur Université Bourgogne Franche-Comté Reviewer

Localization : Amphithéâtre B - Bâtiment Métrologie - UFR ST 16, Route de Gray 25000 Besançon