Vers une formalisation d'une chaîne de compilation pour un ordinateur quantique L'avènement des ordinateurs quantiques capables de résoudre des problèmes irréalisables sur des ordinateurs classiques a motivé le développement de nouveaux langages et outils de programmation pour l'informatique quantique. Cependant, l'état de l'art actuel en matière de programmation quantique n'en est qu'à ses débuts. Dans cette thèse, nous présentons une série d'approches novatrices de différents aspects du processus de compilation quantique basé sur le calcul ZX. Tout d'abord, nous introduisons une nouvelle représentation intermédiaire pour les programmes quantiques capable d'encoder la récursion bornée et les structures de circuits répétés de manière compacte, basée sur les familles de l'extension Scalable du calcul ZX. Nous présentons ensuite un algorithme de compilation pour les circuits hybrides contenant à la fois des portes quantiques et classiques, basé sur l'optimisation de circuits purs de Duncan et al. Enfin, nous définissons le problème de la détection des sections de circuits quantiques qui peuvent être traduites en logique classique, et nous introduisons un algorithme heuristique pour le résoudre.
Vers une formalisation d'une chaîne de compilation pour un ordinateur quantique L'avènement des ordinateurs quantiques capables de résoudre des problèmes irréalisables sur des ordinateurs classiques a motivé le développement de nouveaux langages et outils de programmation pour l'informatique quantique. Cependant, l'état de l'art actuel en matière de programmation quantique n'en est qu'à ses débuts. Dans cette thèse, nous présentons une série d'approches novatrices de différents aspects du processus de compilation quantique basé sur le calcul ZX. Tout d'abord, nous introduisons une nouvelle représentation intermédiaire pour les programmes quantiques capable d'encoder la récursion bornée et les structures de circuits répétés de manière compacte, basée sur les familles de l'extension Scalable du calcul ZX. Nous présentons ensuite un algorithme de compilation pour les circuits hybrides contenant à la fois des portes quantiques et classiques, basé sur l'optimisation de circuits purs de Duncan et al. Enfin, nous définissons le problème de la détection des sections de circuits quantiques qui peuvent être traduites en logique classique, et nous introduisons un algorithme heuristique pour le résoudre.
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.
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 calcul quantique est nouveau paradigme qui sera peut-être en capacité de résoudre certains problèmes intéressants et très spécifiques plus vite qu'un ordinateur classique. Mais pour atteindre le régime dans lequel les ordinateurs quantiques seront plus efficaces que leurs équivalents classiques, plusieurs étapes cruciales doivent être atteintes. Les taux d'erreur des puces quantiques actuelles doivent être drastiquement améliorés, tout comme leur nombre de qubits, les algorithmes doivent évoluer pour prendre en compte le taux d'erreur élevé des puces, les compilateurs et implémentations doivent être adaptés à la puce quantique qui sera utilisée pour l'exécution et les façons d'analyser des états ou programmes quantiques nécessitent des améliorations.Dans cette thèse, nous nous concentrons sur certaines de ces étapes et améliorons l'état de l'art en essayant de se rapprocher le plus possible du régime où les ordinateurs quantiques auront un avantage sur les ordinateurs classiques. Nous commençons par montrer comment nous avons implémenté un algorithme quantique non trivial et analysé son comportement ainsi que les ressources nécessaires à son exécution.Cette analyse a confirmé que les puces quantiques actuelles étaient incapables d'exécuter ce genre d'implémentation, même après avoir pris en compte les subtilités dues au matériel et optimisé grandement le programme. Cet effort d'optimisation a donné lieu à l'implémentation de l'outil qprof, un profileur de programme quantique capable d'analyser des implémentations et de générer un rapport textuel et lisible résumant la hiérarchie des appels et leur coût approximatif.Nous présentons aussi un algorithme classique pour résoudre le problème du routage de qubit, une des étapes les plus coûteuse en terme de porte quantique additionnelle dans les compilateurs de programme quantiques. Cet algorithme permet de prendre en compte les calibrations les plus récentes de la puce quantique visée afin d'adapter le programme quantique compilé aux différents taux d'erreurs de la puce. Nous décrivons comment l'algorithme fonctionne et montrons qu'il apporte une amélioration substantielle de la fidélité de l'état quantique créé par le programme compilé par rapport à l'état de l'art.Nous avons aussi implémenté un algorithme variationnel permettant de résoudre des systèmes linéaires et analysé son comportement sur des puces quantiques actuelles ainsi que les besoins en ressources quantiques afin d'exécuter cet algorithme avec différents systèmes linéaires. Finalement, nous avons effectué une étude sur les erreurs présentes sur des qubits isolés et introduit une nouvelle visualisation permettant de mettre en avant des erreurs systématiques et non mitigées par les calibrations automatiques réalisées à intervalles réguliers sur les puces quantiques.
Le calcul quantique est nouveau paradigme qui sera peut-être en capacité de résoudre certains problèmes intéressants et très spécifiques plus vite qu'un ordinateur classique. Mais pour atteindre le régime dans lequel les ordinateurs quantiques seront plus efficaces que leurs équivalents classiques, plusieurs étapes cruciales doivent être atteintes. Les taux d'erreur des puces quantiques actuelles doivent être drastiquement améliorés, tout comme leur nombre de qubits, les algorithmes doivent évoluer pour prendre en compte le taux d'erreur élevé des puces, les compilateurs et implémentations doivent être adaptés à la puce quantique qui sera utilisée pour l'exécution et les façons d'analyser des états ou programmes quantiques nécessitent des améliorations.Dans cette thèse, nous nous concentrons sur certaines de ces étapes et améliorons l'état de l'art en essayant de se rapprocher le plus possible du régime où les ordinateurs quantiques auront un avantage sur les ordinateurs classiques. Nous commençons par montrer comment nous avons implémenté un algorithme quantique non trivial et analysé son comportement ainsi que les ressources nécessaires à son exécution.Cette analyse a confirmé que les puces quantiques actuelles étaient incapables d'exécuter ce genre d'implémentation, même après avoir pris en compte les subtilités dues au matériel et optimisé grandement le programme. Cet effort d'optimisation a donné lieu à l'implémentation de l'outil qprof, un profileur de programme quantique capable d'analyser des implémentations et de générer un rapport textuel et lisible résumant la hiérarchie des appels et leur coût approximatif.Nous présentons aussi un algorithme classique pour résoudre le problème du routage de qubit, une des étapes les plus coûteuse en terme de porte quantique additionnelle dans les compilateurs de programme quantiques. Cet algorithme permet de prendre en compte les calibrations les plus récentes de la puce quantique visée afin d'adapter le programme quantique compilé aux différents taux d'erreurs de la puce. Nous décrivons comment l'algorithme fonctionne et montrons qu'il apporte une amélioration substantielle de la fidélité de l'état quantique créé par le programme compilé par rapport à l'état de l'art.Nous avons aussi implémenté un algorithme variationnel permettant de résoudre des systèmes linéaires et analysé son comportement sur des puces quantiques actuelles ainsi que les besoins en ressources quantiques afin d'exécuter cet algorithme avec différents systèmes linéaires. Finalement, nous avons effectué une étude sur les erreurs présentes sur des qubits isolés et introduit une nouvelle visualisation permettant de mettre en avant des erreurs systématiques et non mitigées par les calibrations automatiques réalisées à intervalles réguliers sur les puces quantiques.
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.
Les ordinateurs quantiques exploitent les principes de la physique quantique pour encoder et traiter l'information, avec le potentiel de surpasser les capacités des ordinateurs classiques dans certains domaines. Cette thèse explore l'une des technologies majeures du calcul quantique : l'optique linéaire, où les calculs sont effectués à l'aide de photons traversant des circuits d'optique linéaire.Si ces circuits sont bien compris et simulables à petite échelle, leur véritable intérêt apparaît à grande échelle lorsqu'ils atteignent des régimes hors de portée du calcul classique. Cette thèse s'intéresse à cette transition sous deux aspects : sur le plan calculatoire d'une part, en développant des modèles plus efficaces pour repousser les limites des simulations classiques, et sur le plan formel d'autre part, en modélisant à un niveau plus abstrait les circuits optiques et leurs interactions.En simulation, l'un des défis majeurs est le calcul efficace des probabilités de sortie des circuits. Nous présentons dans cette thèse de nouveaux algorithmes pour calculer plusieurs de ces probabilités, où l'utilisation de la mémoire est optimisée pour significativement réduire le temps de calcul. Ce travail mène au développement de Perceval, une plateforme logicielle open-source dédiée au calcul quantique photonique.Sur le plan théorique, nous introduisons un cadre formel et diagrammatique qui capture pleinement la structure des processus d'optique linéaire. Plus précisément, nous utilisons le formalisme des langages graphiques pour modéliser ces circuits. Nous établissons une théorie équationnelle complète, démontrant que deux circuits équivalents d'optique linéaire peuvent toujours être réécrits localement avec notre ensemble d'équations.Enfin, nous montrons comment nos contributions ont des applications à la fois en physique et en informatique quantique théorique. En particulier, nous étendons notre théorie équationnelle complète des circuits optiques à une théorie équationnelle complète pour les circuits quantiques, résolvant ainsi un problème ouvert des dernières décennies.