REVIEW 1 cited by
QWIRE Practice: Formal Verification of Quantum Circuits in Coq
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
We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem proving features. The implementation uses higher-order abstract syntax to represent variable binding and provides a type-checking algorithm for linear wire types, ensuring that quantum circuits are well-formed. We formalize a denotational semantics that interprets QWIRE circuits as superoperators on density matrices, and prove the correctness of some simple quantum programs.
Forward citations
Cited by 1 Pith paper
-
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.
Discussion (0). Continue with ORCID to comment.