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).

翻译：近年来，递归技术被引入量子程序设计领域，使得各类大规模量子线路与算法能够以优雅且经济的方式进行编程。本文提出一种用于形式化验证递归定义量子线路正确性的证明系统。该证明系统的可靠性与（相对）完备性已得到严格证明。为展示其有效性，本文给出了一系列该证明系统的应用实例，包括（多量子比特）受控门、生成（多量子比特）GHZ（Greenberger-Horne-Zeilinger）态的量子线路、量子傅里叶变换的递归定义、量子态制备以及量子随机存取存储器（QRAM）。