Dans le modèle usuel de calcul quantique, des opérations sur des données quantiques sont contrôlées de manière essentiellement classique. Un contrôle lui aussi quantique est cependant possible, mais a été peu étudié en comparaison. En particulier, il manque au contrôle quantique un formalisme permettant de l’exprimer de manière simple afin de raisonner efficacement sur des processus l’impliquant.
La première contribution de cette thèse est de poser les fondations d’un cadre formel dédié au contrôle quantique, sous la forme d’un langage graphique. Notre principal résultat concernant ce langage est l’introduction d’une théorie équationnelle complète, c’est à dire d’un ensemble d’équations permettant de transformer un diagramme, par réécriture locale successive, en n’importe quel autre diagramme représentant le même programme ou processus physique.
Une deuxième contribution est l’application de ce formalisme d’une part au problème de l’optimisation des ressources dans les processus impliquant un contrôle quantique, et d’autre part à la caractérisation de l’équivalence observationnelle des canaux de communication quantiques.
La troisième contribution de cette thèse est l’introduction d’un langage pour les circuits optiques linéaires. Nous l’équipons d’une théorie équationnelle complète, ainsi que d’une forme normale simple, accessible par un système de réécriture fortement normalisant et confluent.
La dernière contribution de cette thèse, peut-être la plus importante, est l’introduction d’une théorie équationnelle complète pour le langage des circuits quantiques. Nous nous appuyons pour cela sur une correspondance entre les circuits quantiques et les circuits optiques, qui nous permet de transférer la théorie équationnelle déjà obtenue pour les circuits optiques.
