Job opportunities
Centres Inria associés
Type de contrat
Contexte
<p><strong>The PhD is funded by funded by PEPR EPiQ will be carried out at Inria Nancy Grand-Est within the Inria mocqua project team.</strong></p>
<p> </p>
<p> </p>
Mission confié
<p>Quantum programming languages with quantum control allow the execution flow of programs to depend on<br />quantum data, enabling superpositions of computational paths, as exemplified by the Quantum Switch [1].<br />While this paradigm provides a natural and expressive way to model quantum computation, it raises<br />fundamental challenges regarding physical implementability and computational complexity. In particular,<br />programs with quantum control must respect both the laws of quantum mechanics and strict resource<br />bounds in order to admit efficient physical realizations.</p>
<p><br />Recent work [2, 3] has shown that type systems inspired by linear logic and realizability techniques can be<br />used to ensure key physical properties of quantum programs, such as unitarity and feasibility. However, the<br />interaction between quantum control, higher-order features, and resource guarantees remains only partially<br />understood. In particular, there is currently no fully satisfactory typed framework that simultaneously<br />supports quantum control, higher-order quantum lambda calculi, and precise certifications of time and space<br />complexity.</p>
<p><br />The goal of this PhD is to develop a typed quantum programming language with quantum control in which<br />resource consumption is certified by construction. The approach will rely on light linear logic and realizability<br />techniques to control duplication and iteration, ensuring that programs normalize within prescribed<br />complexity bounds while remaining physically meaningful.</p>
<p><br />A central objective is to design a type system that characterizes quantum complexity classes such as BQP and<br />FBQP in a sound and complete way. This includes establishing a correspondence between typable programs<br />and families of quantum circuits with polynomial-time (and potentially polynomial-space) bounds, thereby<br />providing an implicit-complexity-style characterization of quantum complexity classes in a higher-order<br />setting.</p>
<p> </p>
<p>References<br />[1] O. Oreshkov, F. Costa and Č. Brukner, “Quantum correlations with no causal order,” Nature Communications, no. 1092, 2012.<br />[2] A. Díaz-Caro, M. Guillermo, A. Miquel and B. Valiron, "Realizability in the Unitary Sphere," in 34th Annual ACM/IEEE Symposium on Logic in<br />Computer Science (LICS), 2019.<br />[3] E. Hainry, R. Péchoux and M. Silva, “Branch Sequentialization in Quantum Polytime,” in 10th International Conference on Formal Structures<br />for Computation and Deduction (FSCD), 2025.</p>
<p><br />Recent work [2, 3] has shown that type systems inspired by linear logic and realizability techniques can be<br />used to ensure key physical properties of quantum programs, such as unitarity and feasibility. However, the<br />interaction between quantum control, higher-order features, and resource guarantees remains only partially<br />understood. In particular, there is currently no fully satisfactory typed framework that simultaneously<br />supports quantum control, higher-order quantum lambda calculi, and precise certifications of time and space<br />complexity.</p>
<p><br />The goal of this PhD is to develop a typed quantum programming language with quantum control in which<br />resource consumption is certified by construction. The approach will rely on light linear logic and realizability<br />techniques to control duplication and iteration, ensuring that programs normalize within prescribed<br />complexity bounds while remaining physically meaningful.</p>
<p><br />A central objective is to design a type system that characterizes quantum complexity classes such as BQP and<br />FBQP in a sound and complete way. This includes establishing a correspondence between typable programs<br />and families of quantum circuits with polynomial-time (and potentially polynomial-space) bounds, thereby<br />providing an implicit-complexity-style characterization of quantum complexity classes in a higher-order<br />setting.</p>
<p> </p>
<p>References<br />[1] O. Oreshkov, F. Costa and Č. Brukner, “Quantum correlations with no causal order,” Nature Communications, no. 1092, 2012.<br />[2] A. Díaz-Caro, M. Guillermo, A. Miquel and B. Valiron, "Realizability in the Unitary Sphere," in 34th Annual ACM/IEEE Symposium on Logic in<br />Computer Science (LICS), 2019.<br />[3] E. Hainry, R. Péchoux and M. Silva, “Branch Sequentialization in Quantum Polytime,” in 10th International Conference on Formal Structures<br />for Computation and Deduction (FSCD), 2025.</p>
Principales activités
<p>More specifically, the PhD will address the following research directions:</p>
<ul>
<li>the design of a typed quantum lambda calculus with quantum control, combining linear and light<br />linear logic modalities with realizability-based semantics, in order to certify polynomial-time<br />normalization of quantum programs;</li>
<li>the development of sound and complete characterizations of quantum complexity classes such as<br />BQP and FBQP via typing disciplines, extending existing first-order or classically controlled results to<br />higher-order and quantum controlled languages;</li>
<li>the identification of a well-behaved fragment of the language in which programs can be compiled<br />into quantum circuits (or alternative low-level models) of polynomial size, preserving both semantics<br />and complexity guarantees;</li>
<li>the extension of the analysis to space complexity, with the aim of controlling and certifying the<br />number of qubits used during program execution.</li>
</ul>
<p>The obtained results will be published in main conferences and main journals of the domain.</p>
<ul>
<li>the design of a typed quantum lambda calculus with quantum control, combining linear and light<br />linear logic modalities with realizability-based semantics, in order to certify polynomial-time<br />normalization of quantum programs;</li>
<li>the development of sound and complete characterizations of quantum complexity classes such as<br />BQP and FBQP via typing disciplines, extending existing first-order or classically controlled results to<br />higher-order and quantum controlled languages;</li>
<li>the identification of a well-behaved fragment of the language in which programs can be compiled<br />into quantum circuits (or alternative low-level models) of polynomial size, preserving both semantics<br />and complexity guarantees;</li>
<li>the extension of the analysis to space complexity, with the aim of controlling and certifying the<br />number of qubits used during program execution.</li>
</ul>
<p>The obtained results will be published in main conferences and main journals of the domain.</p>
Compétences
<p>Technical skills and level required :</p>
<p>Good level in quantum computing</p>
<p>Good level in functional programming</p>
<p>Knowledge on type systems</p>
<p>Knowledge in complexity theory</p>
<p>Languages : english (mandatory) + french</p>
<p> </p>
<p>Good level in quantum computing</p>
<p>Good level in functional programming</p>
<p>Knowledge on type systems</p>
<p>Knowledge in complexity theory</p>
<p>Languages : english (mandatory) + french</p>
<p> </p>
Référence
2026-09727
Thème
Domaine d'activité