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.
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.
Vers une correspondance de Curry-Howard pour le calcul quantique 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.
Combining classical and quantum control : A logical, syntactic and semantic perspective Cette thèse vise principalement à établir les fondements théoriques nécessaires à la conception d'un langage de programmation complet pour l'informatique quantique. L'idée qui a inspiré toutes les contributions de cette thèse est de produire dans le cadre quantique un développement similaire à celui utilisé pour les langages de programmation et la logique dans le paradigme classique. En nous appuyant sur les travaux préparatoires de la correspondance Curry-Howard-Lambek, nous essayons d'approfondir les trois pierres angulaires de cette correspondance : les langages de programmation, la logique et la théorie des catégories, en nous concentrant sur la combinaison de deux paradigmes et en considérant des programmes avec des flots de contrôle quantique et classique. Nous avons essayé d'aller plus loin. Nous avons également abordé les deux visions complémentaires de la mécanique quantique, celles de Heisenberg et de Schrödinger, et adopté l'une d'elles pour définir une sémantique physiquement intuitive pour les langages dont nous discutons. Cette thèse apporte deux contributions principales à la littérature existante sur les langages de programmation quantiques. Nous introduisons tout d'abord un lambda calcul quantique qui combine le contrôle quantique et classique, dont la conception s'appuie sur la structure mathématique de sa sémantique dénotationnelle physiquement intuitive. La sémantique opérationnelle de ce langage est basée sur une adaptation des configurations quantiques que nous introduisons, et est liée au modèle dénotationnel par un résultat d'adéquation. Le langage fournit également un prototype de types inductifs quantiques à travers le type qnat, un type pour les entiers naturels quantiques. Le modèle dénotationnel de ce calcul est basé sur les algèbres de von Neumann, qui sont au cœur de la formulation mathématique de la vision de Heisenberg de la mécanique quantique. La deuxième contribution est un langage de preuve pour le fragment IMALL de la logique linéaire qui s'appuie sur certaines observations clés du calcul présenté ci-dessus. Ce langage estl'un des premiers à pouvoir prendre en charge des programmes combinant des constructions telles que le quantum switch et la mesure. À cet égard, ce travail constitue une amélioration significative par rapport au calcul précédent, car il prend en charge une version plus fine du contrôle quantique, permettant ainsi l'écriture d'algorithmes tels que le quantum switch. La syntaxe du langage est par nature algébrique et linéaire, permettant d'écrire des combinaisons linéaires de termes. Une conséquence majeure, avec la sémantique de la modalité B qu'il introduit, est que la mesure n'est plus une construction de base du langage. Elle peut désormais être écrite comme un programme parmi d'autres dans le langage. Enfin, la sémantique dénotationnelle de ce travail est basée sur les algèbres C* - une généralisation des algèbres de von Neumann. Le modèle dénotationnel s'avère adéquat pour la sémantique opérationnelle, dont la linéarité en est une conséquence naturelle. Enfin, nous concluons cette thèse en présentant les limites de ces travaux et les orientations possibles pour des travaux futurs.
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.
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.
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.