Towards a Curry-Howard Correspondence for Quantum Computation

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.