Le modèle Qram est un modèle de calcul quantique pratique composé d’un ordinateur classique et un processus quantique qui communiquent entre eux. Le programme est exécuté sur l’ordinateur classique. Il envoie les instructions correspondant aux opérateurs quantiques sur le co-processeur, et reçoit le résultat de l’observation de l’état quantique. Ce modèle est considéré comme un modèle standard et plusieurs langages de programmation ont été conçus en basant sur ce modèle. Alors que les programmes dans ce modèle sont capables de réaliser tout calcul quantique grâce à l’usage de la mémoire quantique, il est difficile de les analyser sans l’aide d’un autre ordinateur quantique. Ce problème suscite le besoin pour des méthodes formelles pour les langages programmations quantiques : les outils formels pour raisonner sur l’optimisation du code, pour l’analyser des ressources, et pour spécifier et prouver les propriétés des programmes quantiques. La sémantique catégorique fait partie de ces méthodes qui fait le lien entre les opérateurs quantiques et les programmes et introduit le système logique qui peut décrire les propriétés sur l’état quantique dans le système de types. Bien que plusieurs travaux proposent des sémantiques catégoriques pour les langages de description de circuits quantiques, aucun ne supporte l’usage du résultat d’une mesure au sein du processeur classique (le ”levage dynamique”). Dans cette thèse, nous formalisons le levage dynamique qui transfère le résultat d’observations sur l’état quantique à l’information classique dans un langage de programmation de description de circuit quantique. En suivant l’approche du langage Proto-Quipper, nous définissons un langage typé de description de circuit quantique où l’information quantique levée est incorporée dans la structure ramifiée. Ensuite, le levage dynamique est formalisé dans le cadre de la sémantique opérationnelle et la sémantique catégorique. Notre sémantique catégorique est basée sur le modèle de Francisco Rios et Peter Selinger pour le langage programmation Proto-Quipper- M. Pourtant, pour formaliser le levage dynamique, nous construisons une catégorie de Kleisli en capturant la mesure quantique comme un effet de bord sur une catégorie concrète pour le circuit avec la mesure quantique. Nous prouvons le théorème de correction de la sémantique catégorique par rapport à la sémantique opérationnelle.
Le modèle Qram est un modèle de calcul quantique pratique composé d’un ordinateur classique et un processus quantique qui communiquent entre eux. Le programme est exécuté sur l’ordinateur classique. Il envoie les instructions correspondant aux opérateurs quantiques sur le co-processeur, et reçoit le résultat de l’observation de l’état quantique. Ce modèle est considéré comme un modèle standard et plusieurs langages de programmation ont été conçus en basant sur ce modèle. Alors que les programmes dans ce modèle sont capables de réaliser tout calcul quantique grâce à l’usage de la mémoire quantique, il est difficile de les analyser sans l’aide d’un autre ordinateur quantique. Ce problème suscite le besoin pour des méthodes formelles pour les langages programmations quantiques : les outils formels pour raisonner sur l’optimisation du code, pour l’analyser des ressources, et pour spécifier et prouver les propriétés des programmes quantiques. La sémantique catégorique fait partie de ces méthodes qui fait le lien entre les opérateurs quantiques et les programmes et introduit le système logique qui peut décrire les propriétés sur l’état quantique dans le système de types. Bien que plusieurs travaux proposent des sémantiques catégoriques pour les langages de description de circuits quantiques, aucun ne supporte l’usage du résultat d’une mesure au sein du processeur classique (le ”levage dynamique”). Dans cette thèse, nous formalisons le levage dynamique qui transfère le résultat d’observations sur l’état quantique à l’information classique dans un langage de programmation de description de circuit quantique. En suivant l’approche du langage Proto-Quipper, nous définissons un langage typé de description de circuit quantique où l’information quantique levée est incorporée dans la structure ramifiée. Ensuite, le levage dynamique est formalisé dans le cadre de la sémantique opérationnelle et la sémantique catégorique. Notre sémantique catégorique est basée sur le modèle de Francisco Rios et Peter Selinger pour le langage programmation Proto-Quipper- M. Pourtant, pour formaliser le levage dynamique, nous construisons une catégorie de Kleisli en capturant la mesure quantique comme un effet de bord sur une catégorie concrète pour le circuit avec la mesure quantique. Nous prouvons le théorème de correction de la sémantique catégorique par rapport à la sémantique opérationnelle.
Méthodes Formelles pour les Langages de Programmation Quantiques Le modèle Qram est un modèle de calcul quantique pratique composé d’un ordinateur classique et un processus quantique qui communiquent entre eux. Le programme est exécuté sur l’ordinateur classique. Il envoie les instructions correspondant aux opérateurs quantiques sur le co-processeur, et reçoit le résultat de l’observation de l’état quantique. Ce modèle est considéré comme un modèle standard et plusieurs langages de programmation ont été conçus en basant sur ce modèle. Alors que les programmes dans ce modèle sont capables de réaliser tout calcul quantique grâce à l’usage de la mémoire quantique, il est difficile de les analyser sans l’aide d’un autre ordinateur quantique. Ce problème suscite le besoin pour des méthodes formelles pour les langages programmations quantiques : les outils formels pour raisonner sur l’optimisation du code, pour l’analyser des ressources, et pour spécifier et prouver les propriétés des programmes quantiques. La sémantique catégorique fait partie de ces méthodes qui fait le lien entre les opérateurs quantiques et les programmes et introduit le système logique qui peut décrire les propriétés sur l’état quantique dans le système de types. Bien que plusieurs travaux proposent des sémantiques catégoriques pour les langages de description de circuits quantiques, aucun ne supporte l’usage du résultat d’une mesure au sein du processeur classique (le ”levage dynamique”). Dans cette thèse, nous formalisons le levage dynamique qui transfère le résultat d’observations sur l’état quantique à l’information classique dans un langage de programmation de description de circuit quantique. En suivant l’approche du langage Proto-Quipper, nous définissons un langage typé de description de circuit quantique où l’information quantique levée est incorporée dans la structure ramifiée. Ensuite, le levage dynamique est formalisé dans le cadre de la sémantique opérationnelle et la sémantique catégorique. Notre sémantique catégorique est basée sur le modèle de Francisco Rios et Peter Selinger pour le langage programmation Proto-Quipper- M. Pourtant, pour formaliser le levage dynamique, nous construisons une catégorie de Kleisli en capturant la mesure quantique comme un effet de bord sur une catégorie concrète pour le circuit avec la mesure quantique. Nous prouvons le théorème de correction de la sémantique catégorique par rapport à la sémantique opérationnelle.
Dans cette thèse, nous nous intéressons au développement d'une correspondance de Curry-Howard pour l'informatique quantique, permettant de représenter des types quantiques et le flot de contrôle quantique. Dans le modèle standard de l'informatique quantique, un ordinateur classique est lié à un coprocesseur quantique. L'ordinateur classique peut alors envoyer des instructions pour allouer, mettre à jour ou lire des registres quantiques. Les programmes exécutés par le coprocesseur sont représentés par un circuit quantique : une séquence d'instructions qui applique des opérations unitaires aux registres quantiques. Bien que le modèle soit universel, dans le sens où il peut représenter n'importe quelles opérations unitaire, il reste limité : il lui manque une représentation correcte du flot d'exécution non causal. Normalement, pour représenter le branchement, on peut utiliser un système de type contenant un coproduit, permettant le choix entre deux exécutions possibles, mais les circuits quantiques ne contiennent que des qubits et leurs tenseurs. D'autre part, les types sont fortement liés à la logique à travers la correspondance Curry-Howard qui stipule que les types de programmes correspondent aux formules et les programmes aux preuves, tandis que l'évaluation du programme correspond à la simplification de la preuve correspondante. Bien que cette correspondance ait été étendue à des cas multiples en informatique classique, elle n'a pas encore émergée dans l'informatique quantique. Pour résoudre ces problèmes, nous suivons deux approches différentes : la première, par le développement d'un langage de programmation linéaire et réversible, capturant un sous-ensemble de l'informatique quantique, ainsi qu'une correspondance Curry-Howard avec la logique µMALL. Le langage existe en deux versions : l'une représentant des fonctions réversibles et totales, tandis que l'autre peut représenter des fonctions partielles. Les deux versions sont accompagnées d'un résultat d'expressivité : dans la première, nous pouvons capturer l'ensemble des fonctions primitive récursives, tandis que dans la deuxième, nous montrons comment capturer n'importe quelle Machine de Turing. La deuxième approche suit le développement d'une sémantique à base de jetons, inspirée de la géométrie de l'interaction de Girard, pour des langages graphique pour le calcul quantique. Dans cette approche, une sémantique à base de jetons a été donnée pour le ZX-Calcul : un langage graphique pour l'informatique quantique capable de représenter n'importe quel opérateur linéaire. Nous montrons comment cette nouvelle sémantique correspond à la sémantique dénotationnelle standard. Nous étendons ensuite le ZX-Calcul avec un coproduit et un tenseur explicite dans le développement du Many-Worlds Calcul. Ce nouveau langage est accompagné sémantique dénotationnelle et une théorie équationnelle qui est logiquement correcte et complète. Nous montrons comment le contrôle quantique peut être représenté dans ce système. Enfin, le langage de programmation est modifié dans le cas quantique pur et nous utilisons le Many-Worlds Calculus comme un modèle dénotationnel pour ce nouveau langage de programmation.
Programmation et apprentissage des processeurs quantiques Les avancées significatives en physique atomique, moléculaire et optique qui ont car-actérisé les dernières décennies nous ont offert une multitude de systèmes quantiques àN corps hautement contrôlables. Ce sont des plateformes prometteuses pour réaliser desprocesseurs quantiques, c’est-à-dire des systèmes quantiques qui peuvent être program-més pour simuler la dynamique d’un modèle cible ou pour résoudre des problèmes decalcul complexes. Tout en promettant des simulations quantiques à grande échelle et uncalcul quantique tolérant aux erreurs, cette nouvelle génération de processeurs quantiquessoulève également un certain nombre de défis théoriques. Dans cette thèse, nous nousconcentrons sur deux questions clés : (1) la programmation d’un système quantique avecdes interactions fixes pour réaliser des circuits quantiques et des dynamiques Hamiltoni-ennes, et (2) l’apprentissage de la structure de l’état d’un processeur quantique à partir dedonnées de mesure.Dans la première partie de cette thèse, nous présentons un protocole qui permet deréaliser des dynamiques Hamiltoniennes arbitraires et des circuits quantiques dans lessimulateurs quantiques programmables, en se basant sur le contrôle local de leurs degrésde liberté avec un champ exterieur. En particulier, nous montrons comment cela peut êtrefait via des impulsions temporelles mises au point analytiquement, et donnont des preuvesrigoureuses de garantie de performance. Nous illustrons les applications concrètes de ceprotocole par des exemples dans les contextes de la simulation quantique, de la correctiond’erreur quantique et de l’optimisation quantique. Enfin, inspirés par des travaux expéri-mentaux récents, nous considérons les effets de plusieurs imperfections expérimentales,démontrant ainsi que ces impulsions temporelles sont naturellement robustes. Ceci rendnotre protocole bien adapté aux expériences quantiques actuelles. Il en résulte une ap-proche prometteuse pour réaliser un processeur quantique universel dans des systèmesqui ne permettent pourtant pas un contrôle direct de leurs interactions.Dans la deuxième partie, nous développons de nouvelles méthodes pour caractériserl’état quantique d’un processeur quantique. Nous nous concentrons en particulier surles applications des mesures aléatoires, un formalisme récemment introduit qui permetd’estimer plusieurs propriétés d’un système quantique à partir des corrélations statistiquesentre des mesures quantiques effectuées dans des configurations aléatoires. Nous intro-duisons tout d’abord une quantité capable de classifier le comportement à grande échellede l’intrication dans les états mixtes, et qui peut être estimée à l’aide de mesures aléatoires.Nous étudions le comportement de cette quantité dans des ensembles d’états aléatoiresphysiquement pertinents et montrons comment elle peut être utilisée pour les distinguer.Nous introduisons ensuite une nouvelle méthode d’analyse des mesures aléatoires et mon-trons expérimentalement son application à l’estimation de l’intrication d’opérateurs (op-erator entanglement) dans la dynamique des ions piégés. Enfin, nous présentons un algo-rithme applicable à grande échelle et capable d’apprendre une représentation en termesdes réseaux des tenseurs d’un état quantique à partir de données de mesures aléatoires.Comme cette représentation est pertinente pour un état issu d’une dynamique unidimen-sionnelle bruitée et qu’elle est adaptée à un usage à grande échelle par les ordinateursclassique, cet algorithme est pertinent pour comparer les processeurs quantiques avec des centaines de qubits et pour évaluer l’avantage quantique. Ces résultats étendent la portéedes mesures aléatoires et découvrent de nouvelles applications dans les états quantiquesconstitués de nombreux qubits.
Nous présentons dans cette thèse un nouveau modèlepour les langages de programmation quantique. Notre modèle est uneadaptation de la sémantique de jeux probabilistes définie par Danos etHarmer: nous y ajoutons des stratégies quantiquespour permettre la représentation des états et des opérations quantiques.Nous établissons quelques propriétés de base de ces stratégies. Cespropriétés sont ensuite utilisées pour construire des sémantiquesdénotationnelles pour trois langages de programmation quantique. Le premierlangage est une formalisation du calcul par mesures proposé par Danoset al. Les deux autres langages sont nouveaux: ce sont deslangages quantiques d'ordre supérieur dont la syntaxe a été construiteà partir d'observations expliquant l'échec des tentatives précédentespour construire une sémantique dénotationnelle pour de tels langages. La sémantique de jeux présentée dans cette thèseest la première sémantique dénotationnelle pour de telslambda-calculs équipés de types et d'opérations supplémentairespermettant la programmation d'algorithmes quantiques. Les résultatsprésentés valident les deux approches différentes utilitées dans laconception de ces deux nouveaux languages d'ordre supérieur: une premièreoù les états quantiques sont indirectement accessibles via desréférences et une seconde où ils sont introduit directement comme desconstantes dans le langage. Les stratégies quantiques présentéespermettent de comprendre les contraintes devant êtreimposées aux systèmes de type quantique comportant des types d'ordresupérieurs. La contrainte la plus importante est le fait que l'abstractionsur une partie d'un état quantique comportant plusieurs qbits inconnus doitêtre prohibée. Les stratégies quantiques constituent un nouveau modèle mathématique quidécrit l'interaction entre les données classiques et quantiques par desdialogues entre système et environnement. L'interaction entre les differentespar
Vérification pratique des transformations de circuits quantiques L'informatique quantique, qui repose sur les principes de la physique quantique, promet des gains significatifs en termes de puissance de calcul. Cependant, elle introduit de nouveaux défis, notamment pour la vérification de programmes.En effet, les techniques de vérification classiques ne s'appliquent pas directement à l'informatique quantique. Cela s'explique principalement par l'utilisation de la mémoire quantique (unité d'information non standard) et de son opération de mesure, qui est le seul moyen de récupérer une information à partir d'un bit quantique et introduit un aspect probabiliste.Dans cette thèse, nous nous concentrons sur le modèle de calcul quantique par circuits et sur un aspect pratique de ce modèle : les transformations de circuit.Un circuit quantique peut être purement quantique (circuit unitaire) ou inclure du contrôle classique et de la mesure (circuit hybride).Les transformations de circuits se produisent tout au long du processus de calcul quantique, qu'il s'agisse de compiler un circuit décrit dans un langage de haut niveau vers un langage de bas niveau, d'optimiser un circuit pour un matériel particulier (transpilation), de changer de modèle de calcul (one-way measurement), ou de transférer un état quantique (téléportation).Chacune de ces transformations peut altérer le comportement du circuit ; nous avons donc besoin d'outils permettant de vérifier sa préservation.Mais la plupart des outils actuels sont limités au cas unitaire, donc limités à vérifier des transformations qui ne changent pas le type de circuit : un circuit unitaire est transformé en circuit unitaire.Et ceux qui s'aventurent dans le cas hybride sont limités à l'hybridation : un circuit unitaire est transformé en un circuit hybride.Alors que le vrai défi survient lors de l'introduction de fils auxiliaires, tels que les ancillas ou les discards (mesures intermédiaires non incluses dans la sortie du circuit), car il faut s'assurer que ces fils auxiliaires n'affectent pas les autres.Pour vérifier un circuit, plusieurs techniques existent (simulation, exécution symbolique, preuve), qui diffèrent par leur automatisation et leur scalabilité. La simulation, bien qu'automatisable, manque de scalabilité. L'exécution symbolique, automatisable, passe mieux à l'échelle. La preuve, insensible à l'échelle, est difficile à automatiser.Nous avons ainsi opté pour la preuve et pour l'exécution symbolique.Nous avons utilisé la preuve pour certifier une passe de compilation d'un langage de haut niveau vers un langage de bas niveau. Et l'exécution symbolique, en développant un outil de vérification d'équivalence de circuits hybrides avec discard.Pour nous aider dans la preuve, nous avons utilisé l'outil de preuve semi-automatique Qbricks, capable de prouver des circuits unitaires paramétrés basés sur les sommes de chemins, un formalisme permettant une modélisation compacte et encodable des circuits.En préalable au développement de notre outil de vérification de circuits hybrides avec discard, nous avons défini des relations d'équivalence partielles pour les circuits unitaires, ainsi qu'un mécanisme pour étendre les outils de vérification unitaires aux circuits hybrides.La combinaison de ces deux composants permet de traiter les circuits hybrides avec discard.Pour évaluer notre approche, nous avons implémenté dans l'outil SQbricks nos relations d'équivalence ainsi que notre mécanisme d'extension des outils limités aux unitaires.Nous avons démontré que les outils unitaires étendus au cas hybride sans discard surpassent, pour la plupart, largement l'état de l'art.Et qu'avec l'ajout d'un test de séparation au niveau unitaire, nous pouvons traiter des classes beaucoup plus vastes.
Sémantique des Jeux Quantique Cette thèse porte sur la sémantique des langages de programmation quantiques, et en particulier sur celle du lambda-calcul quantique, un langage paradigmatique dû à Selinger et Valiron qui marrie flot de contrôle classique riche (fonctions d’ordre supérieur, récursion, etc) avec des données quantiques (création de qubits, mesure, application d’opérateurs unitaires). Pour donner un modèle du lambda-calcul quantique, il convient de trouver une alliance harmonieuse entre les modèles traditionnels de sémantique dénotationnelle (qui donnent du sens aux programmes en les interprétant dans des univers mathématiques adéquats) et les mathématiques du quantique (espaces de Hilbert, matrices de densité, etc). Cette thèse comporte trois contributions principales : Premièrement, nous étendons la sémantique des jeux, une approche dynamique à la sémantique dénotationnelle, au cas quantique. Nous obtenons le premier modèle dénotationnel du lambda-calcul quantique complet qui soit à la fois compositionnel et interactif, c’est à dire qu’il représente la dynamique de l’exécution. Notre modèle est une généralisation naturelle de développements récents pour le cas probabiliste.Deuxièmement, nous relions formellement notre modèle au seul modèle dénotationnel pré-existant du lambda-calcul quantique complet, le modèle relationnel quantique dû à Pagani, Selinger et Valiron. Finalement, nous montrons que notre modèle de jeux est pleinement adéquat, la correspondance idéale entre un langage de programmation et sa sémantique dénotationnelle. Nous en déduisons que le modèle relationnel quantique était lui-aussi pleinement adéquat, un problème que ses auteurs avaient laissé ouvert. Cette thèse se décompose en trois parties. La première partie présente des préliminaires de théorie des catégories, qui permettent de définir un cadre formel englobant à la fois notre modèle de jeux quantique et le modèle relationnel quantique, puis des préliminaires sur les mathématiques du quantique, et enfin des préliminaires sur la programmation quantique et ses modèles. La deuxième partie commence par des préliminaires de sémantique des jeux, et définit notre modèle de jeux quantique dans un cadre simplifié : le lambda-calcul linéaire quantique. Enfin, la troisième partie s'appuie sur la deuxième pour présenter le modèle de jeux quantique complet, prouver que ce modèle est pleinement adéquat, et en déduire que le modèle relationnel quantique est lui aussi pleinement adéquat.