REVIEW 2 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
Verification of Recursively Defined Quantum Circuits
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 2 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 ...
-
A Practical Quantum Hoare Logic with Classical Variables, I
Presents a Hoare logic for quantum programs with classical variables using paired classical first-order formulas and quantum predicates, plus a simplified proof system with minimal modifications to classical Hoare logic.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.