De Boutray, Henri
[Author]
;
Bourgogne Franche-Comté
[Contributor];
Giorgetti, Alain
[Contributor];
Holweck, Frédéric
[Contributor];
Masson, Pierre-Alain
[Contributor]
Computational studies of entanglement and quantum contextuality properties towards their formal vérification ; Etudes calculatoires de l'intrication et de la contextualité quantiques dans la perspective de leur vérification formelle
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
Electronic Thesis;
E-Book
Title:
Computational studies of entanglement and quantum contextuality properties towards their formal vérification ; Etudes calculatoires de l'intrication et de la contextualité quantiques dans la perspective de leur vérification formelle
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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. ; Although current quantum computers are limited to the use of a few quantum bits, the ...