Verification of Recursively Defined Quantum Circuits
<|reference_start|>Verification of Recursively Defined Quantum Circuits: Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and economically 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 demonstrating its effectiveness, a series of application examples of the proof system are given, including (multi-qubit) controlled gates, a quantum circuit generating (multi-qubit) GHZ (Greenberger-Horne-Zeilinger) states, recursive definition of quantum Fourier transform, quantum state preparation, and quantum random-access memories (QRAM).<|reference_end|>
@article{ying2024verification,
    title={Verification of Recursively Defined Quantum Circuits},
    author={Mingsheng Ying and Zhicheng Zhang},
    journal={arXiv preprint arXiv:2404.05934},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.05934},
    primaryClass={quant-ph cs.LO cs.PL}
}