A programming language combining quantum and classical control
Kinnari Dave, Louis Lemonnier, Romain Péchoux, Vladimir Zamdzhiev
TL;DR
<3-5 sentence high-level summary> This work addresses the longstanding split between classical-control and quantum-control in quantum programming by proposing a unified language that embeds a pure-quantum-control subsystem inside a classical control framework via a modality that interprets pure quantum types as mixed-state operations in the Heisenberg picture. It develops a rigorous equational theory for the pure fragment and couples it with a main calculus whose operational semantics are expressed through quantum configurations, backed by a denotational model built on von Neumann algebras (facilitated by the $\mathcal B$ functor). The resulting framework supports both pure and mixed-state quantum computation, proves strong normalisation and soundness/adequacy, and accommodates infinite-dimensional data types like $\ell^2(\mathbb{N})$, enabling high-level quantum programming abstractions. The paper illustrates the approach with examples such as teleportation, Bell-state generation, and quantum walks, and discusses the relationship between Heisenberg and Schrödinger viewpoints. It also identifies future directions, including richer inductive types and higher-order pure quantum constructs, to broaden the language’s expressiveness and applicability.
Abstract
The two main notions of control in quantum programming languages are often referred to as "quantum" control and "classical" control. With the latter, the control flow is based on classical information, potentially resulting from a quantum measurement, and this paradigm is well-suited to mixed state quantum computation. Whereas with quantum control, we are primarily focused on pure quantum computation and there the "control" is based on superposition. The two paradigms have not mixed well traditionally and they are almost always treated separately. In this work, we show that the paradigms may be combined within the same system. The key ingredients for achieving this are: (1) syntactically: a modality for incorporating pure quantum types into a mixed state quantum type system; (2) operationally: an adaptation of the notion of "quantum configuration" from quantum lambda-calculi, where the quantum data is replaced with pure quantum primitives; (3) denotationally: suitable (sub)categories of Hilbert spaces, for pure computation and von Neumann algebras, for mixed state computation in the Heisenberg picture of quantum mechanics.