Vers une correspondance de Curry-Howard pour le calcul quantique

In this thesis, we are interested in the development of a Curry-Howard correspondence for quantum computing, allowing to represent quantum types andquantum control-flow. In the standard model of Quantum Computation, a classical computer is linked to a quantum coprocessor. The classical computer can then send instructions to allocate, update, or read quantum registers. The programs executed by the coprocessor are represented by a quantum circuit: a sequence of instructions that applies unitary operations to the input quantum bits. While the model is universal, in the sense that it can represent any unitary operations, it stays limited: it lacks of proper representation of non-causal execution flow. Normally, to represent branching, one can use a type system featuring a coproduct, allowing for the choice between two possible executions, but quantum circuits only feature qubits and tensors thereof. On the other hand, types and strongly related to logic via the Curry-Howard correspondence which states that types of programs correspond to formulas and programs to proofs, while the program evaluation is matched with the proof simplification. While this correspondence has been extended to multiple setting in classical computer, it has yet to emerge in quantum computing. To address those problems we follow two different approaches: the first one, through the development of a linear and reversible programming language,capturing a subset of quantum computing, along with a Curry-Howard correspondence with the logic µMALL. The language comes in two versions: onerepresenting exactly complete, reversible functions while the other one can represent partial functions. Both version comes with an expressivity result: inthe former, one can capture the whole class of Primitive Recursive Functions, while in the later any Turing Machine we show how to capture any Turing Machine. The second approach follows the development of token-based semantics, inspired by Girard's Geometry of Interaction, for graphical language for quantum computation. In this approach, a token-based semantics was given for the ZX-Calculus: a graphical language for quantum computation capable of representing any linear operators. We show how the token-based semantics matches the denotational one. We extend the ZX-Calculus with a coproduct and an explicit tensor in the development of the Many-Worlds Calculus. This new languages comes with a token-based semantics, a denotational semantics and an equational theory that is sound and complete. We show how quantum control can be represented in this system. Finally, the programming language is modified to be able to realize pure quantum computation and the graphical language is then used as a denotational model for it.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