DESCRIPTION :
Quantum programming languages with quantum control allow the execution flow of programs to depend on
quantum data, enabling superpositions of computational paths, as exemplified by the Quantum Switch [1].
While this paradigm provides a natural and expressive way to model quantum computation, it raises
fundamental challenges regarding physical implementability and computational complexity. In particular,
programs with quantum control must respect both the laws of quantum mechanics and strict resource
bounds in order to admit efficient physical realizations.
Recent work [2, 3] has shown that type systems inspired by linear logic and realizability techniques can be
used to ensure key physical properties of quantum programs, such as unitarity and feasibility. However, the
interaction between quantum control, higher-order features, and resource guarantees remains only partially
understood. In particular, there is currently no fully satisfactory typed framework that simultaneously
supports quantum control, higher-order quantum lambda calculi, and precise certifications of time and space
complexity.
The goal of this PhD is to develop a typed quantum programming language with quantum control in which
resource consumption is certified by construction. The approach will rely on light linear logic and realizability
techniques to control duplication and iteration, ensuring that programs normalize within prescribed
complexity bounds while remaining physically meaningful.
A central objective is to design a type system that characterizes quantum complexity classes such as BQP and
FBQP in a sound and complete way. This includes establishing a correspondence between typable programs
and families of quantum circuits with polynomial-time (and potentially polynomial-space) bounds, thereby
providing an implicit-complexity-style characterization of quantum complexity classes in a higher-order
setting.
References
[1] O. Oreshkov, F. Costa and Č. Brukner, "Quantum correlations with no causal order," Nature Communications, no. 1092, 2012.
[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
Computer Science (LICS), 2019.
[3] E. Hainry, R. Péchoux and M. Silva, "Branch Sequentialization in Quantum Polytime," in 10th International Conference on Formal Structures
for Computation and Deduction (FSCD), 2025.
Principales activités
More specifically, the PhD will address the following research directions:
* the design of a typed quantum lambda calculus with quantum control, combining linear and light
linear logic modalities with realizability-based semantics, in order to certify polynomial-time
normalization of quantum programs;
* the development of sound and complete characterizations of quantum complexity classes such as
BQP and FBQP via typing disciplines, extending existing first-order or classically controlled results to
higher-order and quantum controlled languages;
* the identification of a well-behaved fragment of the language in which programs can be compiled
into quantum circuits (or alternative low-level models) of polynomial size, preserving both semantics
and complexity guarantees;
* the extension of the analysis to space complexity, with the aim of controlling and certifying the
number of qubits used during program execution.
Code d'emploi : Thésard (h/f)
Temps partiel / Temps plein : Plein temps
Type de contrat : Contrat à durée indéterminée (CDI)
Compétences : Quantum Computing, Systèmes de Type, Technologies Informatiques, Programmation Fonctionnelle, Programming Languages, Anglais, Français, Sens de la Communication, Travaux de Construction, Processus de Normalisation, Analyse Numérique, Quantum, Comptabilité de la Consommation des Ressources, Sémantique, Dactylographie, Mécanique Quantique
Courriel :
romain.pechoux@loria.fr
Téléphone :
0139635511
Type d'annonceur : Employeur direct
