[PhD 2022] Quantum programming with (co)inductive types

Quantum technologies have led to the emergence of a new promising computational paradigm which can efficiently solve problems considered to be intractable on classical computers. Recent developments highlight the necessity of filling the gap between quantum algorithms and the actual quantum computers on which they have to be executed. As a consequence, quantum programming languages play a key role in the future development of quantum computing.

However, most existing quantum languages are fairly low-level: all of the quantum phenomena which induce computational speedup (compared to classical computation) are restricted to quantum bits, also known as qubits, and the operations which allow us to modify qubits are low-level quantum gates. This low-level machinery, comparable to boolean circuits, requires the programmer to focus on cumbersome architectural details, rather than focusing on algorithmic and high-level patterns. Because of this, there is a strong need to develop high-level quantum programming languages, where phenomena such as superposition and entanglement, are available at higher quantum types, not just qubits.

Towards this direction, quantum types generalizing standard classical ones have to be introduced and corresponding type systems and programming languages for manipulating them have to be studied. These types can be inductively defined, e.g., quantum natural numbers and quantum lists, hence allowing us to form superpositions and entanglement patterns of nats, lists, etc., and not just qubits. Alternatively, they can be coinductively defined, e.g., infinite streams of qubits, which poses difficult research questions for quantum programming language design, due to the infinitary nature of this data. Designing a suitable formalism to solve these issues would have a significant impact on quantum programming languages and would enable programmers to write high-level and more concise code.

Project description:

This PhD project aims at studying substructural and quantum type systems with inductive and coinductive types. The applicant will design and study the type-theoretic, operational and denotational aspects of the corresponding languages and systems. Towards that end, particular attention will be paid to the following tasks:

1. Design a quantum programming language with (co)inductive types and a type-safe operational semantics, where superposition and entanglement are first-class resources available at all types, not just qubits.
2. Define a suitable denotational (i.e., mathematical) semantics of this language and demonstrate its soundness and adequacy with respect to the operational semantics.
3. Study important behavioral properties of this language, such as productivity and complexity.

References :

[1] P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14:4, 2004.

[2] P. Selinger, B. Valiron. A lambda calculus for quantum computation with classical control. Mathematcal Structures in Computer Science, 16:3, 2006.

[3] R. Péchoux, S. Perdrix, M. Rennela, V. Zamdzhiev. Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory. FoSSaCS 2020.

[4] B. Lindenhovius, M. W. Mislove, V. Zamdzhiev. Mixed linear and non-linear recursive types. ICFP 2019.

[5] R. Clouston, A. Bizjak, H. B. Grathwohl, L. Birkedal. Programming and Reasoning with Guarded Recursion for Coinductive Types. FoSSaCS 2015.

[6] R. Atkey, C. McBride. Productive coprogramming with guarded recursion. ICFP 2013.

[7] R. Péchoux. Implicit Computational Complexity: Past and Future. Habilitation thesis. Université de Lorraine, 2020.

[8] M. Avanzini, G. Moser, R. Péchoux, S. Perdrix, V. Zamdzhiev. Quantum Expectation Transformers for Cost Analysis, 2022.

The PhD student will be coadvised by Romain Péchoux (Associate Professor, HDR, Université de Lorraine, 50%) et Vladimir Zamdzhiev (Researcher, Inria, 50%) in the Inria team mocqua.