REVIEW 4 cited by
Verification of Recursively Defined Quantum Circuits
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original abstract
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).
Forward citations
Cited by 4 Pith papers
-
Higher-Order Programs with Indefinite Causal Orders: a Linear Approach to Coherent Control of Quantum Processes
A linear-typed higher-order language realises indefinite causal orders on general quantum channels (including measurements), with soundness in Caus[CPM] and expressivity covering all first-order channels plus a large ...
-
Laws of Quantum Programming
A formally verified collection of algebraic laws, normal forms, and a tail-recursion theorem for quantum programs, generalizing Hoare's classical laws.
-
ReOC: Compilation of Recursive Quantum Oracles with Recursion-Aware Uncomputation
A compilation framework from the new language RQIMP to the existing RQC++ language compiles recursive quantum oracles with quantum-controlled recursion and adds recursion-aware automatic uncomputation.
-
High-level quantum structured programs as quantum registers compositions
A formal framework for structured quantum programming where operations act on entire quantum registers, demonstrated by a quantum SMT solver prototype.
Discussion (0). Continue with ORCID to comment.