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:2408.10054 · Proceedings of the ACM on Programming Languages

Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs

Zhicheng Zhang, Mingsheng Ying

Published Jun 10, 2025• 4 citations
arXivHTMLPDF

Abstract

Quantum recursive programming has been recently introduced for describing sophisticated and complicated quantum algorithms in a compact and elegant way. However, implementation of quantum recursion involves intricate interplay between quantum control flow and recursive procedure calls. In this paper, we aim at resolving this fundamental challenge and develop a series of techniques to efficiently implement quantum recursive programs. Our main contributions include:

DOI
10.1145/3729283

Related papers

A Logic for Recursive Quantum Programs

Zhaowei Xu, Mingsheng Ying, Shenggang Ying

Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of non-recursive quantum programs. However, there are as yet no general methods for reasoning about recursive procedures in quantum computing. We fill the gap in this paper by presenting a logic for recursive quantum programs. This logic is an extension of quantum Hoare logic for quantum While-programs. The (relative) completeness of the logic is proved, and its effectiveness is shown by a running example: fixed-point Grover's search.

arXiv:1812.00349•Dec 2, 2018•0 citations

Formal Methods for Quantum Programs: A Survey

Christophe Chareton, Sébastien Bardin, Dong-Ho Lee +3 more

While recent progress in quantum hardware open the door for significant speedup in certain key areas (cryptography, biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is achallenge. Moreover, importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case, due to the destructive aspect of quantum measurement. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. Recent works initiate solutions for problems occurring at every stage of the development process: high-level program design, implementation, compilation, etc. We review the induced challenges for an efficient use of formal methods in quantum computing and the current most promising research directions.

arXiv:2109.06493•Sep 14, 2021•9 citations

Verification of Recursively Defined Quantum Circuits

Mingsheng Ying, Zhicheng Zhang

Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and compactly programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstrate its effectiveness, we present a series of application examples, including formal verification of multi-qubit controlled gates, a quantum circuit for generating multi-qubit GHZ (Greenberger-Horne-Zeilinger) states, and more sophisticated quantum algorithms with recursive structures such as the quantum Fourier transform, quantum state preparation, and quantum random access memories (QRAMs).

arXiv:2404.05934•Proceedings of the ACM on Programming Languages•Jun 8, 2026•0 citations

Quantum implementation of elementary arithmetic operations

Giuseppe Florio, DOMENICO PICCA

Quantum computation has received great attention in recent years for its possible application to difficult problem in classical calculation. Despite the experimental problems of implementing quantum devices, theoretical physicists have tried to conceive some implementations for quantum algorithms. We present here some explicit schemes for executing elementary arithmetic operations.

arXiv:quant-ph/0403048•Mar 5, 2004•14 citations

ReOC: Compilation of Recursive Quantum Oracles with Recursion-Aware Uncomputation

Huiling Wu, Yuxin Deng

Quantum oracles are essential to many quantum algorithms, and their specifications may involve recursive control flow that depends on runtime quantum data. However, existing reversible compilation frameworks provide limited support for such quantum-controlled recursive structures. We present ReOC, a compilation framework that transforms high-level recursive oracle specifications with quantum control flow into reversible quantum programs. The framework comprises RQIMP, a high-level imperative source language for specifying recursive oracles, and a method of compiling programs in that language into RQC++, an existing high-level quantum recursive language with quantum control flow. In this way, we avoid the tedious and error-prone process of directly writing quantum oracles in RQC++. To manage static storage under dynamic quantum control, ReOC uses an indexed static-register discipline to isolate live variables across recursion layers, enabling safe register reuse while controlling quantum storage usage. Furthermore, to address the exponential time blow-up caused by naive uncomputation in recursive settings, ReOC employs a recursion-aware uncomputation strategy: temporary variables from recursive calls are cleaned using deferred strategies to control time overhead, while those from non-recursive statements are cleaned eagerly to reduce space usage. For linear recursion, this strategy yields overhead linear in recursion depth, parameterized by the per-layer register footprint and primitive-operation costs. Finally, we provide a mathematical proof of compilation correctness from RQIMP to RQC++, establishing semantic preservation and correct uncomputation of temporary quantum variables.

arXiv:2608.07973•Aug 8, 2026•0 citations

Tutorials

Quantum computers offer the potential to extend our abilities to tackle computational problems in fields such as number theory, encryption, search and scientific computation.Up to a superpolynomial speedup has been reported for quantum algorithms in these areas.Motivated by the promise of faster computations, the development of quantum machines has caught the attention of both academics and industry researchers.Quantum machines are now at sizes where implementations of quantum algorithms or their components are now becoming possible.In order to implement quantum algorithms on quantum machines, resource efficient circuits and functional blocks must be designed.This tutorial will cover the following:

IEEE International Symposium on Smart Electronic Systems (iSES)•Dec 1, 2022•0 citations
Quantum recursive programming has been recently introduced for describing sophisticated and complicated quantum algorithms in a compact and elegant way. However, implementation of quantum recursion involves intricate interplay between quantum control flow and recursive procedure calls. In this paper, we aim at resolving this fundamental challenge and develop a series of techniques to efficiently implement quantum recursive programs. Our main contributions include:
Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of non-recursive quantum programs. However, there are as yet no general methods for reasoning about recursive procedures in quantum computing. We fill the gap in this paper by presenting a logic for recursive quantum programs. This logic is an extension of quantum Hoare logic for quantum While-programs. The (relative) completeness of the logic is proved, and its effectiveness is shown by a running example: fixed-point Grover's search.
While recent progress in quantum hardware open the door for significant speedup in certain key areas (cryptography, biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is achallenge. Moreover, importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case, due to the destructive aspect of quantum measurement. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. Recent works initiate solutions for problems occurring at every stage of the development process: high-level program design, implementation, compilation, etc. We review the induced challenges for an efficient use of formal methods in quantum computing and the current most promising research directions.
Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and compactly programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstrate its effectiveness, we present a series of application examples, including formal verification of multi-qubit controlled gates, a quantum circuit for generating multi-qubit GHZ (Greenberger-Horne-Zeilinger) states, and more sophisticated quantum algorithms with recursive structures such as the quantum Fourier transform, quantum state preparation, and quantum random access memories (QRAMs).
Quantum oracles are essential to many quantum algorithms, and their specifications may involve recursive control flow that depends on runtime quantum data. However, existing reversible compilation frameworks provide limited support for such quantum-controlled recursive structures. We present ReOC, a compilation framework that transforms high-level recursive oracle specifications with quantum control flow into reversible quantum programs. The framework comprises RQIMP, a high-level imperative source language for specifying recursive oracles, and a method of compiling programs in that language into RQC++, an existing high-level quantum recursive language with quantum control flow. In this way, we avoid the tedious and error-prone process of directly writing quantum oracles in RQC++. To manage static storage under dynamic quantum control, ReOC uses an indexed static-register discipline to isolate live variables across recursion layers, enabling safe register reuse while controlling quantum storage usage. Furthermore, to address the exponential time blow-up caused by naive uncomputation in recursive settings, ReOC employs a recursion-aware uncomputation strategy: temporary variables from recursive calls are cleaned using deferred strategies to control time overhead, while those from non-recursive statements are cleaned eagerly to reduce space usage. For linear recursion, this strategy yields overhead linear in recursion depth, parameterized by the per-layer register footprint and primitive-operation costs. Finally, we provide a mathematical proof of compilation correctness from RQIMP to RQC++, establishing semantic preservation and correct uncomputation of temporary quantum variables.
Quantum computers offer the potential to extend our abilities to tackle computational problems in fields such as number theory, encryption, search and scientific computation.Up to a superpolynomial speedup has been reported for quantum algorithms in these areas.Motivated by the promise of faster computations, the development of quantum machines has caught the attention of both academics and industry researchers.Quantum machines are now at sizes where implementations of quantum algorithms or their components are now becoming possible.In order to implement quantum algorithms on quantum machines, resource efficient circuits and functional blocks must be designed.This tutorial will cover the following: