[PhD 2024] A quantum programming language with coherent control

Spécialité Informatique
Equipe MOCQUA
Encadrement de la thèse Romain PECHOUX   Co-Directeur Simon PERDRIX
Starting date 1 september 2024
Application deadline (à 23h59) 30 april 2024
Profile and skills required
Basic knowledge of:
-quantum computing
-programming languages
Project description
The development of quantum programming languages that include quantum control primitives is one of the most important problems in quantum computing [1,2,3]. Quantum control is a central feature in quantum computing that allows programming quantum operations based on quantum data: during program execution, quantum control can allow quantum superpositions of evolutions that depend on a quantum state and, therefore, provides all the quantum functionality that a programmer may want to access.

One of the major difficulties to face when dealing with the development of such programming languages is to ensure the feasibility of programs. This consists in checking that the written programs do not violate the laws of quantum mechanics. A fundamental example of quantum control is the quantum switch [4] which inputs two quantum evolutions U and V, and a control qubit, and consists in applying U followed by V or V followed by U depending on the state of the control qubit. The quantum switch cannot be arbitrarily applied to any quantum evolution on two qubits, as the corresponding program may have no physical meaning. Consequently, an important issue is to design programming languages with suitable restrictions, guaranteeing their valid evolution.

In this PhD, we would like to solve this issue by contributing to the development of programming languages with both quantum control and physical meaning. The studied restrictions can be of distinct nature, e.g., syntactic constraints, specific set of generators, or type systems. As an illustrative example, one could think of a type system ensuring that a multi-qubit operation is non-signaling, that is, the operation can be expressed as A ⊗ B → A’ ⊗ B’ and no information can flow from A to B’ or from B to A’.

We would like also to consider a compilation process to a relevant low-level model to be determined, e.g., quantum circuits [5] or the PBS-calculus [6], thus providing physical implementations of high-level programs. Ideally, the considered model will have nice complexity properties and allow us to represent programs efficiently. Successful completion of this thesis should lead to a better understanding of the physical limits of programming languages, and to progress towards the development of higher-order programming languages with quantum control.

References
[1] Sabry, Amr, Benoît Valiron, and Juliana Kaizer Vizzotto. ‘From symmetric pattern-matching to quantum control.’ FOSSACS 2018.

[2] Díaz-Caro, Alejandro, and Octavio Malherbe. ‘Quantum control in the unitary sphere: Lambda-S1 and its categorical model.’ Logical Methods in Computer Science 18 (2022).

[3] Voichick, Finn, et al. ‘Qunity: A Unified Language for Quantum and Classical Computing.’ Proceedings of the ACM on Programming Languages 7.POPL (2023): 921-951.

[4] Giulio Chiribella, Giacomo Mauro D’Ariano, Paolo Perinotti, and Benoit Valiron. Quantum computations without definite causal structure. Physical Review A, 88:2, 2013.

[5] Nielsen, Michael A., and Isaac L. Chuang. ‘Quantum computation and quantum information.’ Phys. Today 54.2 (2001): 60.

[6] Clément, Alexandre, and Simon Perdrix. ‘PBS-calculus: A graphical language for coherent control of quantum computations.’ MFCS 2020.