Henri De Boutray : " Études calculatoires de l'intrication et de la contextualité quantiques dans la perspective de leur vérification formelle"

Résumé : Bien que les ordinateurs quantiques actuels se limitent à l'utilisation de quelques qubits, les fondations de la programmation quantique se sont développées au cours des 20 dernières années. Ces fondations ont été théorisées dès les années 80 mais la complexité de leur mise en œuvre a rendu ces pistes inaccessibles jusqu'à très récemment. Dans ce contexte, l'objectif de cette thèse est de contribuer à l'adaptation des méthodes de spécification formelle et de vérification déductive des programmes classiques aux programmes quantiques. Je présente donc mes contributions à l'étude des propriétés quantiques dans le but de les formaliser. J'étudie en particulier l'intrication quantique et la contextualité quantique. Ces propriétés permettent de classifier les états et les protocoles quantiques, et en particulier de les différencier des états et protocoles classiques. Mon étude de l'intrication est fondée plus spécifiquement sur l'évolution de l'intrication au cours de deux algorithmes quantiques : l'algorithme de Grover et la transformée de Fourier quantique. Pour quantifier l'intrication le long de ces algorithmes, j'utilise des polynômes de Mermin, qui ont l'avantage de pouvoir être implémentables dans des ordinateurs quantiques réels. Mon étude de la contextualité s'appuie, elle, sur des géométries finies représentant des expériences, qui sont dites contextuelles quand aucune théorie classique non-contextuelle ne peut en prédire les résultats. Ces géométries sont associées à des espaces polaires symplectiques binaires dont nous explorons la structure, avec comme objectif d'utiliser cette structure pour obtenir des intuitions sur les protocoles quantiques en utilisant la contextualité. L'étude de ces propriétés a conduit à des conjectures intéressantes que nous avons commencé à formaliser dans des environnements de preuve tels que Coq et Why3, mais qui sont laissées en perspective car ces travaux n'ont pas encore abouti.

Composition du jury :

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

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