Doctorant F/H Langage de programmation quantique garantissant la polynomialité des circuits

Les algorithmes quantiques sont habituellement représentés par des circuits quantiques [Deu89]. Cette représentation ne permet pas d’utiliser des constructions de programmation de haut-niveau telles que les types de données ou les structures de contrôle. C’est pourquoi des langages de programmation quantiques ont été proposés [Sel04]. Parmi les développements récents, [CSV23] propose un langage qui permet de programmer des programmes réversibles et linéaires. Ce langage présente des constructions pour encoder les opérations unitaires. Ces constructions permettent d’effectuer du pattern matching réversible et, de ce fait, peuvent être vues comme des formes spécifiques systèmes de réécriture de termes.

Les systèmes de réécriture de termes définissent un programme via un ensemble de règles de réécriture. De nombreux travaux ont permis de certifier la terminaison et des résultats de complexité sur ces systèmes [BMM11 ; MP09]. Ces travaux utilisent des outils, appelés interprétation (quasi-interprétations, sup-interprétations) qui, combinées avec des techniques de terminaison (Recursive Path Ordering, Multiset Path Ordering), permettent de caractériser la classe des fonctions calculables en temps polynomial et celle des fonctions calculables en espace polynomial.

En informatique quantique, la complexité est définie en premier lieu à l’aide de machine de Turing quantiques (QTM) ou de famille de circuits quantiques. La classe de complexité naturelle est FBQP (Bounded-error Quantum Polynomial time) qui considère les fonctions qui s’exécutent en temps polynomial sur une QTM et donnent le bon résultat dans au moins 2/3 des cas. Cette notion de complexité correspond également aux fonctions qui peuvent être réalisées par une famille uniforme de circuits quantiques dont la taille augmente polynomialement avec le nombre de qubits. Plusieurs travaux récents [Yam20 ; HPS23] ont proposé des caractérisations de FBQP basées sur des algèbres de fonctions et des langages de programmation.

Références

[BMM11]Guillaume Bonfante, Jean-Yves Marion et Jean-Yves Moyen. « Quasi-interpretations a way to control resources ». In : Theoretical Computer Science 412.25 (juin 2011), p. 2776-2796. issn : 0304-3975. doi : 10.1016/j.tcs.2011.02.007.
[CSV23]Kostia Chardonnet, Alexis Saurin et Benoît Valiron. « A Curry-Howard Correspondence for Linear, Reversible Computation ». In : 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). T. 252. 2023, 13:1-13:18. doi : 10.4230/LIPIcs.CSL.2023.13.
[Deu89]David Elieser Deutsch. « Quantum computational networks ». In : Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences 425.1868 (1989), p. 73-90. url : https://www.jstor.org/stable/2398494.
[HPS23]Emmanuel Hainry, Romain Péchoux et Mário Silva. « A programming language characterizing quantum polynomial time ». In : Foundations of Software Science and Computation Structures (FoSSaCS 23). Paris, France, avr. 2023. doi : 10.1007/978-3-031-30829-1_8.
[MP09]Jean-Yves Marion et Romain Péchoux. « Sup-interpretations, a semantic method for static analysis of program resources ». In : ACM Transactions on Computational Logic 10.4 (août 2009), p. 1-31. issn : 1557-945X. doi : 10.1145/1555746.1555751.
[Sel04]Peter Selinger. « Towards a quantum programming language ». In : Mathematical Structures in Computer Science 14.4 (2004), p. 527-586. doi : 10.1017/S0960129504004256.
[Yam20]Tomoyuki Yamakami. « A schematic definition of quantum polynomial time computability ». In : Journal of Symbolic Logic 85.4 (2020), p. 1546-1587. doi : 10.1017/jsl.2020.45.

Nous chercherons à développer des analyses statiques permettant de caractériser des classes de complexité quantique comme FBQP ainsi que de déterminer les ressources (temps, nombre de qubits, ...) utilisées par un programme quantique.

Une première étape consistera à définir un langage de programmation et des contraintes sur ses programmes pour garantir que les fonctions calculées respectent les lois de la mécanique quantique : l’impossibilité de dupliquer un qubit, la réversibilité, l’unitarité des programmes.

Dans une deuxième étape, nous développerons les techniques permettant de garantir la complexité des programmes. Par exemple, en étendant les méthodes basées sur des techniques d’interprétations de programmes au cadre quantique.

Un dernier objectif consistera à certifier des propriétés de complexité des circuits quantiques obtenus par compilation des programmes. Par exemple en garantissant la polynomialité du nombre de portes quantiques utilisées par le circuit.

Compétences techniques :

• Informatique quantique
• Méthodes formelles
• Principes des Langages de Programmation

Langues :

Français/Anglais

• Restauration subventionnée
• Transports publics remboursés partiellement
• Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
• Possibilité de télétravail (après 6 mois d'ancienneté) et aménagement du temps de travail
• Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
• Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
• Accès à la formation professionnelle
• Sécurité sociale

2100€ brut/mois la 1ère année