Doctorant F/H Langage de programmation quantique garantissant la polynomialité des circuits
Contract type : Fixed-term contract
Level of qualifications required : Graduate degree or equivalent
Fonction : PhD Position
Assignment
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.
Main activities
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.
Skills
Compétences techniques :
- Informatique quantique
- Méthodes formelles
- Principes des Langages de Programmation
Langues :
Français/Anglais
Benefits package
- 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
Remuneration
2100€ brut/mois la 1ère année
General Information
- Theme/Domain : Proofs and Verification
- Town/city : Villers lès Nancy
- Inria Center : Centre Inria de l'Université de Lorraine
- Starting date : 2024-10-01
- Duration of contract : 3 years
- Deadline to apply : 2024-04-28
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.
Instruction to apply
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Contacts
- Inria Team : MOCQUA
-
PhD Supervisor :
Hainry Emmanuel / emmanuel.hainry@loria.fr
About Inria
Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.