Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2607.15873

Programming with Quantum-Controlled Quantum Channels

Kengo Hirata, Takeshi Tsukada

cs.PLcs.LOquant-phSubmitted Jul 17, 2026• Announced Jul 20, 2026• 0 citations
arXivHTMLPDF

Abstract

In contrast to a classical bit, which can only take the value $0$ or $1$, its quantum counterpart -- a qubit -- can exist in a superposition of $0$ and $1$. This is a superposition of data values, naturally raising the question of whether one can superpose not only data but also programs. For example, a particular superposition of programs, known as the quantum SWITCH, has attracted much attention, and its implementations and computational advantages have been studied extensively within the physics community. A naive way to control a program by a qubit is by means of a controlled operation. Given an operation $F$, this amounts to considering an operation that behaves as $F$ when the control qubit is $|1\rangle$, and as the identity operation when the control qubit is $|0\rangle$. This idea works well when $F$ is a unitary operation, but it is not well-defined for a general quantum channel. By contrast, the quantum SWITCH is free from the well-definedness issue. This contrast leads to the key insight of this paper: controlled operations and the quantum SWITCH should be regarded as different kinds of quantum control mechanisms. Building on this insight, we develop a novel quantum programming language with quantum control and measurement that can express the quantum SWITCH over quantum channels. Using a semantic analysis based on program transformations, we identify the source of the ill-behavedness of controlled operations as the \emph{correspondence problem}: a lack of coordination between the measurements performed in the then- and else-branches of quantum conditional branching. We address this problem with a linear type system that enforces alignment of the quantum operations used in the two branches, yielding a well-behaved language capable of expressing the quantum SWITCH.

Comments
56 pages

Related papers

Quantum Control Machine: The Limits of Control Flow in Quantum Programming

Charles Yuan, Agnes Villanyi, Michael Carbin

Quantum algorithms for tasks such as factorization, search, and simulation rely on control flow such as branching and iteration that depends on the value of data in superposition. High-level programming abstractions for control flow, such as switches, loops, and higher-order functions, are ubiquitous in classical languages. By contrast, many quantum languages do not provide high-level abstractions for control flow in superposition, and instead require the use of hardware-level logic gates to implement such control flow. The reason for this gap is that whereas a classical computer supports control flow using a program counter that can depend on data, the typical architecture of a quantum computer does not provide a program counter that can depend on data in superposition. As a result, the complete set of control flow abstractions that can be correctly realized on a quantum computer has not yet been established. In this work, we provide a complete characterization of the properties of control flow abstractions that are correctly realizable on a quantum computer. First, we prove that even on a quantum computer whose program counter exists in superposition, one cannot correctly realize control flow in quantum algorithms by lifting the classical conditional jump instruction to work in superposition. This theorem denies the ability to directly lift general abstractions for control flow such as the $λ$-calculus from classical to quantum programming. In response, we present the necessary and sufficient conditions for control flow to be correctly realizable on a quantum computer. We introduce the quantum control machine, an instruction set architecture featuring a conditional jump that is restricted to satisfy these conditions. We show how this design enables a developer to correctly express control flow in quantum algorithms using a program counter in place of logic gates.

arXiv:2304.15000•Apr 28, 2023•2 citations

Quantum Control and General Recursion Beyond the Unitary Case

Kathleen Barsse, Romain Péchoux, Simon Perdrix

Coherent control, aka quantum control, is a central concept in quantum computing that is attracting increasing attention from both the quantum foundations and quantum software communities. Defining coherent control in the presence of recursion and measurement has long been known to be a major challenge. In particular, no-go results have been established for standard semantical domains like completely positive maps. We address this problem by introducing the first quantum programming language with recursion that allows for the coherent control of arbitrary quantum operations. We equip this language with both an operational and a denotational semantics that we prove to be adequate. To design these semantics, we show that combining coherent control, recursion, and measurement crucially requires describing the evolution of subprograms in the absence of input. To address this, the operational semantics takes into account a default evolution branch, while the denotational semantics uses the concept of coherent quantum operation, based on vacuum extensions. We strengthen the validity of our approach by developing an observational equivalence: two programs are equivalent if their probability of termination is the same in any context. The denotational semantics is shown to be fully abstract with respect to this observational equivalence.

arXiv:2507.10466•Leibniz international proceedings in informatics•Jul 14, 2025•0 citations

Higher-Order Programs with Indefinite Causal Orders: a Linear Approach to Coherent Control of Quantum Processes

Kathleen Barsse, Romain Péchoux, Simon Perdrix

Processes with indefinite causal orders (ICOs), such as the quantum switch, are higher-order quantum processes that superpose the order in which quantum operations are performed. Such coherent control yields computational advantages but is not faithfully captured by existing quantum programming languages: either they are restricted to the unitary case, and thus cannot combine ICOs with measurement, or they treat coherent control nonlinearly. In both cases, they do not realize the full computational power of ICOs. We introduce a higher-order quantum functional language that supports general quantum computation, not merely the permutation of channels, and whose linear type system allows quantum control to be well-defined beyond the unitary case, on arbitrary quantum channels. We equip this language with a small-step operational semantics that synchronizes measurement outcomes across superposed branches, using device references and a memory function. We also give a denotational semantics by means of completely positive maps. With linearity as the only constraint, some well-typed terms would denote unphysical maps. We therefore impose a typing discipline that goes beyond linearity, and interpret programs in the causal category Caus[CPM], under which every well-typed program is physically meaningful, a property that can be checked statically and efficiently. We prove soundness, and study the language's expressive power: it can express every quantum channel at first order, and at second order a large subclass of the so-called quantum circuits with quantum control (QC-QCs), containing the quantum switch. Last but not least, we show that this language is well-designed enough to be extended to the nonlinear setting with recursion.

cs.LOCross-listedarXiv:2607.09534•Jul 13, 2026•0 citations

Quantum Control Machine: The Limits of Control Flow in Quantum Programming

Charles Yuan, Agnes Villanyi, Michael Carbin

Quantum algorithms for tasks such as factorization, search, and simulation rely on control flow such as branching and iteration that depends on the value of data in superposition. High-level programming abstractions for control flow, such as switches, loops, higher-order functions, and continuations, are ubiquitous in classical languages. By contrast, many quantum languages do not provide high-level abstractions for control flow in superposition, and instead require the use of hardware-level logic gates to implement such control flow. The reason for this gap is that whereas a classical computer supports control flow abstractions using a program counter that can depend on data, the typical architecture of a quantum computer does not analogously provide a program counter that can depend on data in superposition. As a result, the complete set of control flow abstractions that can be correctly realized on a quantum computer has not yet been established. In this work, we provide a complete characterization of the properties of control flow abstractions that are correctly realizable on a quantum computer. First, we prove that even on a quantum computer whose program counter exists in superposition, one cannot correctly realize control flow in quantum algorithms by lifting the classical conditional jump instruction to work in superposition. This theorem denies the ability to directly lift general abstractions for control flow such as the λ-calculus from classical to quantum programming. In response, we present the necessary and sufficient conditions for control flow to be correctly realizable on a quantum computer. We introduce the quantum control machine, an instruction set architecture featuring a conditional jump that is restricted to satisfy these conditions. We show how this design enables a developer to correctly express control flow in quantum algorithms using a program counter in place of logic gates.

Proceedings of the ACM on Programming Languages•Apr 29, 2024•9 citations

Quantum Alternation: Prospects and Problems

Costin Bădescu, Prakash Panangaden

We propose a notion of quantum control in a quantum programming language which permits the superposition of finitely many quantum operations without performing a measurement. This notion takes the form of a conditional construct similar to the IF statement in classical programming languages. We show that adding such a quantum IF statement to the QPL programming language simplifies the presentation of several quantum algorithms. This motivates the possibility of extending the denotational semantics of QPL to include this form of quantum alternation. We give a denotational semantics for this extension of QPL based on Kraus decompositions rather than on superoperators. Finally, we clarify the relation between quantum alternation and recursion, and discuss the possibility of lifting the semantics defined by Kraus operators to the superoperator semantics defined by Selinger.

arXiv:1511.01567•Electronic Proceedings in Theoretical Computer Science•Nov 3, 2015•26 citations

Combiner le contrôle classique et quantique : une perspective logique, syntaxique et sémantique

Kinnari Vijay Dave

The focus of this thesis is on laying the theoretical foundation for designing an all-encompassing programming language for quantum computing. The idea inspiring all the contributions of this thesis was to mirror the development of programming languages and logic done for classical computing for its quantum counterpart. Following the groundwork of the Curry-Howard-Lambek correspondence, we try to delve into the three cornerstones of this correspondence - programming languages, logic and category theory with a focus on combining two paradigms of control flow in programs - quantum and classical into one framework. We have tried to achieve more. We have also touched upon the two complementary view of quantum mechanics- Heisenberg and Schrödinger, and adopted one view to define a physically intuitive semantics for the languages we discuss. There are two main contributions that this thesis makes to the existing literature on quantum programming languages. We first introduce a quantum lambda calculus which combines quantum and classical control, whose design is guided by the mathematical structure of its physically intuitive denotational semantics. The operational semantics for this language, is based on an adaptation of quantum configurations which we introduce, and is tied to the denotational model through an adequacy result. The language also provides a prototype of quantum inductive types through the type qnat- a type for quantum natural numbers. The denotational model for this calculus is based on von Neumann algebras- which are at the heart of the mathematical formulation of the Heisenberg view of quantum mechanics. The second contribution is a proof language for the IMALL fragment of Linear logic which builds on some key observations from the calculus introduced above. This language is one of the first such works to be able to support programs which combine constructs such as the quantum switch with measurement. In this aspect, this work is a strict improvement on the previous calculus, since it supports a more fine grained version of quantum control, thus enabling expression of algorithms such as the well-known quantum switch. The syntax is also linear algebraic in nature, supporting linear combinations of terms. A key consequence of this, along with the semantics of the B modality that it introduces is that measurement is no longer a ground construct of the language. In fact, it can now be written as just another program in the language. Finally, the denotational semantics for this work is based on C*-algebras - a generalization of von Neumann algebras. The denotational model is shown to be adequate for the operational semantics, whose linearity turns out to be a natural consequence of this. Finally, we conclude this thesis with limitations of these works and possible directions for future work.

•Dec 17, 2025•0 citations
In contrast to a classical bit, which can only take the value 000 or 111, its quantum counterpart -- a qubit -- can exist in a superposition of 000 and 111. This is a superposition of data values, naturally raising the question of whether one can superpose not only data but also programs. For example, a particular superposition of programs, known as the quantum SWITCH, has attracted much attention, and its implementations and computational advantages have been studied extensively within the physics community.
A naive way to control a program by a qubit is by means of a controlled operation. Given an operation FFF, this amounts to considering an operation that behaves as FFF when the control qubit is ∣1⟩|1\rangle∣1⟩, and as the identity operation when the control qubit is ∣0⟩|0\rangle∣0⟩. This idea works well when FFF is a unitary operation, but it is not well-defined for a general quantum channel. By contrast, the quantum SWITCH is free from the well-definedness issue. This contrast leads to the key insight of this paper: controlled operations and the quantum SWITCH should be regarded as different kinds of quantum control mechanisms.
Building on this insight, we develop a novel quantum programming language with quantum control and measurement that can express the quantum SWITCH over quantum channels. Using a semantic analysis based on program transformations, we identify the source of the ill-behavedness of controlled operations as the \emph{correspondence problem}: a lack of coordination between the measurements performed in the then- and else-branches of quantum conditional branching. We address this problem with a linear type system that enforces alignment of the quantum operations used in the two branches, yielding a well-behaved language capable of expressing the quantum SWITCH.
Quantum algorithms for tasks such as factorization, search, and simulation rely on control flow such as branching and iteration that depends on the value of data in superposition. High-level programming abstractions for control flow, such as switches, loops, and higher-order functions, are ubiquitous in classical languages. By contrast, many quantum languages do not provide high-level abstractions for control flow in superposition, and instead require the use of hardware-level logic gates to implement such control flow. The reason for this gap is that whereas a classical computer supports control flow using a program counter that can depend on data, the typical architecture of a quantum computer does not provide a program counter that can depend on data in superposition. As a result, the complete set of control flow abstractions that can be correctly realized on a quantum computer has not yet been established. In this work, we provide a complete characterization of the properties of control flow abstractions that are correctly realizable on a quantum computer. First, we prove that even on a quantum computer whose program counter exists in superposition, one cannot correctly realize control flow in quantum algorithms by lifting the classical conditional jump instruction to work in superposition. This theorem denies the ability to directly lift general abstractions for control flow such as the λλλ-calculus from classical to quantum programming. In response, we present the necessary and sufficient conditions for control flow to be correctly realizable on a quantum computer. We introduce the quantum control machine, an instruction set architecture featuring a conditional jump that is restricted to satisfy these conditions. We show how this design enables a developer to correctly express control flow in quantum algorithms using a program counter in place of logic gates.
Coherent control, aka quantum control, is a central concept in quantum computing that is attracting increasing attention from both the quantum foundations and quantum software communities. Defining coherent control in the presence of recursion and measurement has long been known to be a major challenge. In particular, no-go results have been established for standard semantical domains like completely positive maps. We address this problem by introducing the first quantum programming language with recursion that allows for the coherent control of arbitrary quantum operations. We equip this language with both an operational and a denotational semantics that we prove to be adequate. To design these semantics, we show that combining coherent control, recursion, and measurement crucially requires describing the evolution of subprograms in the absence of input. To address this, the operational semantics takes into account a default evolution branch, while the denotational semantics uses the concept of coherent quantum operation, based on vacuum extensions. We strengthen the validity of our approach by developing an observational equivalence: two programs are equivalent if their probability of termination is the same in any context. The denotational semantics is shown to be fully abstract with respect to this observational equivalence.
Processes with indefinite causal orders (ICOs), such as the quantum switch, are higher-order quantum processes that superpose the order in which quantum operations are performed. Such coherent control yields computational advantages but is not faithfully captured by existing quantum programming languages: either they are restricted to the unitary case, and thus cannot combine ICOs with measurement, or they treat coherent control nonlinearly. In both cases, they do not realize the full computational power of ICOs. We introduce a higher-order quantum functional language that supports general quantum computation, not merely the permutation of channels, and whose linear type system allows quantum control to be well-defined beyond the unitary case, on arbitrary quantum channels. We equip this language with a small-step operational semantics that synchronizes measurement outcomes across superposed branches, using device references and a memory function. We also give a denotational semantics by means of completely positive maps. With linearity as the only constraint, some well-typed terms would denote unphysical maps. We therefore impose a typing discipline that goes beyond linearity, and interpret programs in the causal category Caus[CPM], under which every well-typed program is physically meaningful, a property that can be checked statically and efficiently. We prove soundness, and study the language's expressive power: it can express every quantum channel at first order, and at second order a large subclass of the so-called quantum circuits with quantum control (QC-QCs), containing the quantum switch. Last but not least, we show that this language is well-designed enough to be extended to the nonlinear setting with recursion.
Quantum algorithms for tasks such as factorization, search, and simulation rely on control flow such as branching and iteration that depends on the value of data in superposition. High-level programming abstractions for control flow, such as switches, loops, higher-order functions, and continuations, are ubiquitous in classical languages. By contrast, many quantum languages do not provide high-level abstractions for control flow in superposition, and instead require the use of hardware-level logic gates to implement such control flow. The reason for this gap is that whereas a classical computer supports control flow abstractions using a program counter that can depend on data, the typical architecture of a quantum computer does not analogously provide a program counter that can depend on data in superposition. As a result, the complete set of control flow abstractions that can be correctly realized on a quantum computer has not yet been established. In this work, we provide a complete characterization of the properties of control flow abstractions that are correctly realizable on a quantum computer. First, we prove that even on a quantum computer whose program counter exists in superposition, one cannot correctly realize control flow in quantum algorithms by lifting the classical conditional jump instruction to work in superposition. This theorem denies the ability to directly lift general abstractions for control flow such as the λ-calculus from classical to quantum programming. In response, we present the necessary and sufficient conditions for control flow to be correctly realizable on a quantum computer. We introduce the quantum control machine, an instruction set architecture featuring a conditional jump that is restricted to satisfy these conditions. We show how this design enables a developer to correctly express control flow in quantum algorithms using a program counter in place of logic gates.
We propose a notion of quantum control in a quantum programming language which permits the superposition of finitely many quantum operations without performing a measurement. This notion takes the form of a conditional construct similar to the IF statement in classical programming languages. We show that adding such a quantum IF statement to the QPL programming language simplifies the presentation of several quantum algorithms. This motivates the possibility of extending the denotational semantics of QPL to include this form of quantum alternation. We give a denotational semantics for this extension of QPL based on Kraus decompositions rather than on superoperators. Finally, we clarify the relation between quantum alternation and recursion, and discuss the possibility of lifting the semantics defined by Kraus operators to the superoperator semantics defined by Selinger.
The focus of this thesis is on laying the theoretical foundation for designing an all-encompassing programming language for quantum computing. The idea inspiring all the contributions of this thesis was to mirror the development of programming languages and logic done for classical computing for its quantum counterpart. Following the groundwork of the Curry-Howard-Lambek correspondence, we try to delve into the three cornerstones of this correspondence - programming languages, logic and category theory with a focus on combining two paradigms of control flow in programs - quantum and classical into one framework. We have tried to achieve more. We have also touched upon the two complementary view of quantum mechanics- Heisenberg and Schrödinger, and adopted one view to define a physically intuitive semantics for the languages we discuss. There are two main contributions that this thesis makes to the existing literature on quantum programming languages. We first introduce a quantum lambda calculus which combines quantum and classical control, whose design is guided by the mathematical structure of its physically intuitive denotational semantics. The operational semantics for this language, is based on an adaptation of quantum configurations which we introduce, and is tied to the denotational model through an adequacy result. The language also provides a prototype of quantum inductive types through the type qnat- a type for quantum natural numbers. The denotational model for this calculus is based on von Neumann algebras- which are at the heart of the mathematical formulation of the Heisenberg view of quantum mechanics. The second contribution is a proof language for the IMALL fragment of Linear logic which builds on some key observations from the calculus introduced above. This language is one of the first such works to be able to support programs which combine constructs such as the quantum switch with measurement. In this aspect, this work is a strict improvement on the previous calculus, since it supports a more fine grained version of quantum control, thus enabling expression of algorithms such as the well-known quantum switch. The syntax is also linear algebraic in nature, supporting linear combinations of terms. A key consequence of this, along with the semantics of the B modality that it introduces is that measurement is no longer a ground construct of the language. In fact, it can now be written as just another program in the language. Finally, the denotational semantics for this work is based on C*-algebras - a generalization of von Neumann algebras. The denotational model is shown to be adequate for the operational semantics, whose linearity turns out to be a natural consequence of this. Finally, we conclude this thesis with limitations of these works and possible directions for future work.