[Sujet de thèse 2022] Programmation quantique avec types (co)inductifs

Les technologies quantiques ont permis l’émergence d’un nouveau paradigme computationnel prometteur qui peut résoudre efficacement des problèmes considérés comme insolubles sur des ordinateurs classiques. Les développements récents soulignent la nécessité de combler le fossé entre les algorithmes quantiques et les ordinateurs quantiques réels sur lesquels ils doivent être exécutés. De ce fait, les langages de programmation quantique jouent un rôle clé dans le développement futur de l’informatique quantique.

Cependant, la majorité des langages quantiques existants sont de bas niveau : tous les phénomènes quantiques qui induisent une amélioration des performances calculatoires (par rapport au ordinateurs classiques) sont limités aux bits quantiques, également appelés qubits, et les opérations qui nous permettent de modifier les qubits sont des portes quantiques de bas niveau. Cette mécanique de bas niveau, comparable aux circuits booléens, oblige le programmeur à se concentrer sur des détails architecturaux encombrants, plutôt que sur des modèles algorithmiques de haut niveau. Pour cette raison, il est indispensable de développer des langages de programmation quantique de haut niveau, dans lesquels des phénomènes tels que la superposition et l’intrication sont disponibles pour des types quantiques supérieurs, et pas seulement pour les qubits.

Dans cette optique, il convient d’introduire des types de données quantiques généralisant les types classiques standard et d’étudier les systèmes de types et les langages de programmation correspondants pour les manipuler. Ces types de données peuvent être définis par induction: on peut penser, par exemple, aux nombres naturels quantiques et aux listes quantiques ; ce qui nous permet de former des superpositions et des modèles d’intrication de nombres naturels, de listes, etc. et pas seulement de qubits. Ces types de données peuvent également être définis de manière coinductive : on peut penser, par exemple, à des streams infinis (listes infinies) de qubits. Ceci pose des questions de recherche difficiles pour la conception de langages de programmation quantiques, en raison de la nature infinitaire de ces données. La conception d’un formalisme approprié pour résoudre ces problèmes aurait un impact significatif sur les langages de programmation quantique et permettrait aux programmeurs d’écrire du code de haut niveau et plus concis. Nous aborderons ces problématiques dans le cadre de ce doctorat.

Description du projet :

Ce projet de thèse vise à étudier les systèmes de types quantiques avec des types inductifs et coinductifs. Le candidat concevra et étudiera les aspects théoriques des types de données, opérationnels et dénotationnels des langages et systèmes correspondants. A cette fin, une attention particulière sera accordée aux tâches suivantes :

1. Concevoir un langage de programmation quantique avec des types (co)inductifs et une sémantique opérationnelle correcte du point de vue des types, où la superposition et l’intrication sont des ressources de première classe disponibles pour tous les types, et pas seulement pour les qubits.
2. Définir une sémantique dénotationnelle (c’est-à-dire mathématique) appropriée de ce langage et démontrer sa solidité et son adéquation par rapport à la sémantique opérationnelle.
3. Étudier les propriétés comportementales importantes de ce langage, telles que la productivité et la complexité.

Références bibliographiques :

[1] P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14:4, 2004.

[2] P. Selinger, B. Valiron. A lambda calculus for quantum computation with classical control. Mathematcal Structures in Computer Science, 16:3, 2006.

[3] R. Péchoux, S. Perdrix, M. Rennela, V. Zamdzhiev. Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory. FoSSaCS 2020.

[4] B. Lindenhovius, M. W. Mislove, V. Zamdzhiev. Mixed linear and non-linear recursive types. ICFP 2019.

[5] R. Clouston, A. Bizjak, H. B. Grathwohl, L. Birkedal. Programming and Reasoning with Guarded Recursion for Coinductive Types. FoSSaCS 2015.

[6] R. Atkey, C. McBride. Productive coprogramming with guarded recursion. ICFP 2013.

[7] R. Péchoux. Implicit Computational Complexity: Past and Future. Habilitation thesis. Université de Lorraine, 2020.

[8] M. Avanzini, G. Moser, R. Péchoux, S. Perdrix, V. Zamdzhiev. Quantum Expectation Transformers for Cost Analysis, 2022.

Cette thèse sera co-encadrée par Romain Péchoux (EC, HDR, Université de Lorraine, 50%) et Vladimir Zamdzhiev (ISFP, Inria, 50%) dans l’équipe Inria mocqua.