Pith. sign in

REVIEW 3 major objections 4 minor 47 references

Borrowing Dirty Qubits in Quantum Programs

T0 review · 3 major / 4 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper defines safe uncomputation of dirty qubits in quantum programs and proves that, for circuits made of NOT and multi-controlled NOT gates, safety reduces to two Boolean unsatisfiability checks.

desk verdict Original, useful SAT-based verification for dirty qubits in classical circuits, but the general finite-state theorem (6.1) is not proven as written and needs repair before the theory catches up with the claims. read the letter →

arxiv 2508.17190 v1 pith:4AZI5UL6 submitted 2025-08-24 quant-ph cs.PL

Bonan Su , Li Zhou , Yuan Feng , Mingsheng Ying This is my paper · ORCID
classification quant-phcs.PL MSC 68Q1268Q60
keywords dirtyqubitssafeuncomputationquantumprogramminglanguagescircuitverificationBooleansatisfiabilityqubitreuseancilladenotationalsemantics
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper gives quantum programming a formal way to borrow dirty qubits—ancilla qubits that may start in any state, including entangled ones—and to know when a borrow is safe. Safety means the borrowed qubit is returned exactly as found, so that no experiment can tell it was used. For circuits built only from NOT and multi-controlled NOT gates, the paper shows that checking safety reduces to two classical Boolean unsatisfiability questions. The authors implement this reduction and report that it scales to constant adders with hundreds of qubits and multi-controlled NOT circuits with thousands of qubits. If correct, this turns a quantum verification problem into a task for ordinary SAT solvers.

What carries the argument

The central machinery is the denotational semantics of the borrow statement, which nondeterministically selects a qubit from the syntactically computed idle set $\mathit{idle}(S)$, together with a Boolean-formula tracking scheme for classical circuits. Each qubit $q$ is assigned a Boolean formula $b_q$ updated by the rules for $X$ gates and multi-controlled NOT gates. Formula (6.1) checks that $q$'s final Boolean value implies its initial value, and formula (6.2) checks that when $q$ is in $|+\rangle$, the outputs of all other qubits are independent of $q$. The paper also proves a finite-state refinement (Theorem 6.1): general safe uncomputation can be verified using only five one-qubit states, and for classical circuits only $|0\rangle$ and $|+\rangle$ suffice.

What would settle it

Take a classical circuit with a borrowed qubit, such as the five-qubit example in the paper's Figure 1.4, and run the reduction: if a SAT solver reports both formulas (6.1) and (6.2) unsatisfiable while a direct simulation of the circuit on the state $|+\rangle$ shows that the borrowed qubit's reduced state is changed, the central theorem is false. More generally, brute-force search over small classical circuits can look for a circuit whose two Boolean formulas are both unsatisfiable but whose unitary is not of the form $V\otimes I_q$.

Watch

Extended reading notes

Core claim

A QBorrow program $S$ safely uncomputes a qubit $q$ if and only if every quantum operation in its denotational semantics factors as $I_q \otimes E'$ acting on the other qubits; equivalently, $q$ is restored for any pure input state and its external entanglement is preserved. For circuits implementing classical functions, the paper proves that only two input states need to be checked: $|0\rangle$ and $|+\rangle$. Restoration of $|0\rangle$ becomes the Boolean formula (6.1), and restoration of $|+\rangle$ becomes formula (6.2), which requires the final state of every other qubit to be independent of $q$'s initial value. Theorem 6.4 states that the circuit safely uncomputes $q$ if and only if both formulas are unsatisfiable.

Load-bearing premise

The load-bearing premise is that the syntactically computed set of idle qubits faithfully describes which qubits are actually available at runtime, including the assumption that a nested borrow can reuse the same physical qubit sequentially; if a qubit looks idle but is entangled with the surrounding computation, the verification could certify a borrow that is not safe in practice.

Editorial extensions

If this is right

  • Compilers for quantum programming languages can automatically verify borrow statements before allowing dirty-qubit reuse, instead of assuming safety by construction.
  • Safe uncomputation can be checked per dirty qubit individually, so a program may safely borrow some qubits while other borrows in the same program remain unsafe.
  • The finite-state refinement means full verification never requires enumerating all pure states: five basis states suffice in general, and two suffice for classical circuits.
  • The experimental results indicate that verification overhead grows polynomially with circuit size for the benchmarks, making the approach practical on current hardware.
  • Because safe uncomputation preserves external entanglement, verified dirty-qubit borrows are candidates for use in multi-program scheduling, where disturbing another program's qubits would cause errors.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the syntactically defined idle set were replaced with a runtime-aware resource manager that tracks dynamic entanglement, the same SAT reduction could plausibly be lifted to dynamic scheduling; the paper does not develop this direction.
  • The two-state criterion for classical circuits suggests a testable extension: circuits made of Clifford gates plus classical controls might also admit a finite-state reduction, using the fact that $|+\rangle$ and $|0\rangle$ are stabilizer states.
  • Theorem 6.4 applies to circuits without borrow statements; extending the reduction to circuits that themselves contain nested borrows would require composing Boolean checks across instantiations, a natural next step not covered by the paper.
  • The semantics could serve as a specification for a type-and-effect system that statically enforces safe dirty-qubit borrowing, turning the verification result into a compile-time discipline rather than a post-hoc check.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper extends the quantum programming language QWhile with a borrow/release construct for dirty qubits, giving a denotational semantics in which programs denote sets of quantum operations and a borrowed qubit is nondeterministically chosen from a syntactically computed idle set. It defines safe uncomputation of a dirty qubit q as the requirement that every execution act as the identity on q, and it states equivalences with restoration of arbitrary pure states, preservation of external entanglement, and determinism of the program. For verification, the paper claims a general finite-state reduction (Theorem 6.1), and for circuits made of X and multi-controlled NOT gates it reduces safe uncomputation to checking two Boolean formulas (Theorems 6.2 and 6.4). Experiments on constant adders and multi-controlled-NOT circuits show the SAT/SMT-based verifier scaling to hundreds and thousands of qubits, respectively. An artifact appendix provides the QBorrow grammar, benchmark programs, and build instructions.

Significance. If the theoretical claims are repaired, this is a useful contribution: it gives the first formal language-level account of dirty-qubit borrowing, a clean definition of safe uncomputation, and an efficient, parameter-free verification method for the practically important class of classical reversible circuits. The SAT reduction is a genuine algorithmic idea, and the reported experiments on adders and MCX circuits support the scalability claim for those families. The paper also ships an artifact with grammar files, benchmark programs, and build instructions, which is a strength. The main risk is not in the classical-circuit fragment but in the general finite-state and entanglement-preservation theorems, whose proofs have gaps.

major comments (3)
  1. [Section 9.4, proof of Theorem 6.1, direction (2)⇒(1)] The step asserting that nonzero Hilbert–Schmidt overlap of |−⟩⟨−| with the basis {|0⟩⟨0|,|1⟩⟨1|,|+⟩⟨+|,|+i⟩⟨+i|} implies ρ0=ρ1=ρ+=ρ+i=ρ− is incorrect. In that basis, |−⟩⟨−| = (|0⟩⟨0|+|1⟩⟨1|−|+⟩⟨+|)/2, so the coefficient of |+i⟩⟨+i| is exactly zero; the |−⟩ input only relates ρ0, ρ1, and ρ+, and gives no constraint on ρ+i. Additionally, the proof silently strengthens the hypothesis: condition (5.1) only asserts preservation of the reduced state on q, whereas the proof writes E(ρ⊗|ψ⟩⟨ψ|)=ρψ⊗|ψ⟩⟨ψ|. For these reasons, condition (2) of Theorem 6.1 is not established as a sufficient criterion, and the general claim that safe uncomputation of arbitrary finite-dimensional QBorrow programs can be checked on the finite set ℬ is unsupported as written.
  2. [Section 9.4, proof of Theorem 6.1, direction (3)⇒(1)] There is a nontrivial gap in deriving the factorization (E_k⊗I)(|i⟩⊗(|00⟩+|11⟩)) = |β_{i,k}⟩⊗(|00⟩+|11⟩) for each Kraus operator E_k. The hypothesis only fixes the partial trace of the sum over k, and it is not automatic that each term individually factorizes in this way; one must argue that a positive sum of rank-one terms with a pure partial trace forces each term's partial trace to be proportional to that same pure state. This is likely repairable, but the proof as written omits the argument.
  3. [Section 9.2, proof of Theorem 5.4] The proof of Theorem 5.4 only gives the forward (⇒) direction and stops at the end of that direction; there is no (⇐) argument. Since the theorem states an equivalence between safe uncomputation and preservation of external entanglement, the converse must either be proved or explicitly derived from Theorem 5.3 or another stated result. As it stands, the entanglement-preservation characterization is unproven.
minor comments (4)
  1. [Theorem 6.1, item 3] The expression ρ′ ∈ ℬ^{⊗(n−2)} is not defined for n=1 or n=2; the low-dimensional base cases of the statement should be handled explicitly or excluded.
  2. [Section 6.1, formula (6.2)] The intuitive explanation of condition (6.2) says only that the final states of the other qubits must be independent of the initial value of q; it omits the injectivity argument that also forces the final value of q itself to be toggled, which is needed for the two branches to recombine into |+⟩ rather than into |0⟩. The formulas appear correct, but the accompanying text should make this point.
  3. [Section 4.2 / Figure 4.2] The definition of idle(borrow a; S; release a) = idle(S) and the use of substitution S[q/a] deserve a short formal clarification, especially for nested borrows: the reader must verify that a qubit selected for an inner borrow is excluded from the inner body only after substitution, while remaining available for the outer computation after release. The example in Figure 4.4 is helpful but the general definition should state this more explicitly.
  4. [Section 6.2, experimental results] The sentence in the introduction that the experimental results “provide an affirmative answer to the most pressing research question in quantum verification” is an overstatement; the experiments support scalability for two circuit families, not a general resolution of quantum verification scalability.

Circularity Check

0 steps flagged · score 1.0 of 10

No material circularity: the safe-uncomputation definition, equivalence theorems, and SAT reduction are derived rather than assumed.

full rationale

The paper's central chain is Definition 5.1 (safe uncomputation means E = I_q ⊗ E' for every execution), Theorem 5.3 (equivalence with pure-state restoration), Theorem 6.1 (finite-state refinement), and Theorem 6.4 (reduction to unsatisfiability of formulas (6.1) and (6.2)). None of these steps reduces by construction to its own inputs. Definition 5.1 is a definition, not a derived prediction; Theorem 5.3 is proved from the definition rather than assumed; and the SAT reduction translates the circuit's Boolean behavior into formulas whose unsatisfiability is shown equivalent to the two state-restoration conditions of Theorem 6.2. The experiments verify adder and MCX circuits against these formulas using external solvers; there are no fitted parameters that are later relabeled as predictions. The self-citations to QWhile [38,39] and to the semantic approach of [10] provide background and host-language conventions, but the denotational semantics of QBorrow is fully specified in Figures 4.2 and 4.3, so those citations are not load-bearing for the new results. There is a serious proof concern in Section 9.4: the claim that nonzero overlap of |−⟩⟨−| with |+i⟩⟨+i| forces ρ_{+i}=ρ_− is not logically valid, since the coefficient of |+i⟩⟨+i| in |−⟩⟨−| is zero, and the proof also silently strengthens the reduced-state hypothesis into a product-output conclusion. That is a correctness or completeness gap in a finite-state reduction argument, but it is not a circularity: the theorem is not being defined into existence, and the classical SAT result is proved separately in Theorem 6.4. Accordingly, the paper shows no significant circularity; the score reflects only the background self-citation, which is not load-bearing.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No fitted parameters or new physical entities appear in the paper. The contributions are semantic definitions and proof-based verification, so the free-parameter count is zero. The main load-bearing assumptions are standard quantum information axioms plus the syntactic idleness modeling choice.

assumptions (5)
  • standard math Quantum states are partial density operators on a finite-dimensional Hilbert space, and quantum operations are completely positive trace non-increasing maps.
    Section 2 and the denotational semantics in Figure 4.3 rely on this framework; it is standard quantum information theory.
  • standard math Stinespring dilation and the Kraus representation exist for every quantum operation in the semantics.
    Used in the proofs of Theorems 5.3 and 6.1 in Sections 9.1 and 9.4 to factor an operation as I_q tensor E'.
  • domain assumption The syntactically computed idle set idle(S) is a faithful model of the qubits actually available for borrowing at runtime, and nested borrow statements may reuse the same physical qubit sequentially.
    Section 4.2 defines borrow semantics as union over q in idle(S); Figure 4.4 relies on q3 being borrowable for both a1 and a2. If actual availability is dynamic, the semantics can permit borrows that a runtime would reject.
  • domain assumption For circuits composed only of X and multi-controlled-NOT gates, the unitary is a permutation and final bit values are Boolean functions of initial bits, so the SAT update rules in Section 6.1 fully determine circuit behavior.
    This is the scope restriction for the SAT reduction in Theorems 6.2 and 6.4; outside this class the reduction is not proved.
  • standard math The one-qubit density basis B = {|0><0|,|1><1|,|+><+|,|+i><+i|} spans the one-qubit operator space, and the five test states span the one-qubit state space.
    Used in Theorem 6.1 to reduce verification to finite cases. The spanning property is standard, though the proof's overlap statement about |-> and |+> is not accurate.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Borrowing Dirty Qubits in Quantum Programs." pith.science (2026). https://pith.science/paper/4AZI5UL6

@misc{pith2026250817190,
  author       = {Pith},
  title        = {Pith review of: Borrowing Dirty Qubits in Quantum Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4AZI5UL6}},
  note         = {Machine review of arXiv:2508.17190}
}
read the original abstract

Dirty qubits are ancillary qubits that can be borrowed from idle parts of a computation, enabling qubit reuse and reducing the demand for fresh, clean qubits-a resource that is typically scarce in practice. For such reuse to be valid, the initial states of the dirty qubits must not affect the functionality of the quantum circuits in which they are employed. Moreover, their original states, including any entanglement they possess, must be fully restored after use-a requirement commonly known as safe uncomputation. In this paper, we formally define the semantics of dirty-qubit borrowing as a feature in quantum programming languages, and introduce a notion of safe uncomputation for dirty qubits in quantum programs. We also present an efficient algorithm, along with experimental results, for verifying safe uncomputation of dirty qubits in certain quantum circuits.

Figures

Figures reproduced from arXiv: 2508.17190 by the authors.

Figure 1.1
Figure 1.1. Costs associated with various implementations of addition |𝑎⟩ ↦→ |𝑎 + 𝑐⟩ of a value 𝑎 by a classical constant 𝑐. arithmetic circuits [12, 15] [PITH_FULL_IMAGE:figures/full_fig_p001_1_1.png] view at source ↗
Figure 1
Figure 1. with four working qubits [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 1.2
Figure 1.2. Borrowing idle qubits as dirty ancillas for reuse. safe uncomputation of dirty qubits is a non-trivial task and may be counterintuitive. Consider the circuit for the three￾controlled NOT (CCCNOT) gate shown in [PITH_FULL_IMAGE:figures/full_fig_p002_1_2.png] view at source ↗
Figures from the paper (11 more)
Figure 3
Figure 3. Figure 3: b. Similarly, since [PITH_FULL_IMAGE:figures/full_fig_p004_3.png]
Figure 3.1
Figure 3.1. Figure 3.1: Reducing the number of required qubits through borrowing dirty qubits. the same functionality of [PITH_FULL_IMAGE:figures/full_fig_p005_3_1.png]
Figure 4.1
Figure 4.1. Figure 4.1: Syntax of QBorrow. the lifetime of each borrowed qubit using the syntac￾tic construct borrow 𝑎; . . . ; release 𝑎, analogous to the way variable lifetimes are delineated in classical programming languages; and 2. Instead of assuming safe uncomputation a priori, the s…
Figure 4.2
Figure 4.2. Figure 4.2: Definition of idle-qubit scope. either a concrete element of qubits or a formal placeholder 𝑎 introduced by the borrow 𝑎 statements discussed in the next paragraph. Since each unitary operator 𝑈 and measurement M acts on a fixed number of qubits, called its domain, w…
Figure 4.4
Figure 4.4. Figure 4.4: QBorrow program for [PITH_FULL_IMAGE:figures/full_fig_p007_4_4.png]
Figure 6.1
Figure 6.1. Figure 6.1: Construction of Boolean formulas for a three￾controlled NOT gate. unsatisfiability of the Boolean formula ¬(𝑏𝑞 → 𝑞), (6.1) where → denotes logical implication. By the truth table of implication, (6.1) is unsatisfiable if and only if 𝑞 = 0 implies 𝑏𝑞 = 0. The second c…
Figure 6.2
Figure 6.2. Figure 6.2: Implementation of adder circuits in QBorrow. them. It can be verified that the circuit acts as the identity on qubits 𝑎[1], . . . , 𝑎[𝑛] and 𝑞[1], . . . , 𝑞[𝑛−1], while writing the most significant bit of the sum (𝑠1 . . . 𝑠𝑛)2 + (11 . . . 1)2 into 𝑞[𝑛], where the in…
Figure 6.3
Figure 6.3. Figure 6.3: Verification overhead of adder circuits. 500 1,000 1,500 2,000 2,500 3,000 3,500 0 30 60 90 120 150 180 210 240 Number of qubits Verification Duration (s) CVC5 Bitwuzla [PITH_FULL_IMAGE:figures/full_fig_p011_6_3.png]
Figure 6.4
Figure 6.4. Figure 6.4: Verification overhead of MCX circuits. adder circuit and a single dirty qubit in the MCX circuits, respectively. The verification time includes only the duration taken by the SMT solvers to check the satisfiability of the resulting formulas, which constitutes the mai…
Figure 10.4
Figure 10.4. Figure 10.4: Circuit for the MCX program adapted from [11]. Its implementation in QBorrow can be found in the file QBorrow/examples/mcx.qbr as shown below: 1 // mcx.qbrs 2 let m = 1750; 3 let n = m + (m - 1); // n-controlled NOT gate 4 5 borrow@ q[n]; 6 borrow@ t; 7 8 borrow anc…
Figure 10.1
Figure 10.1. Figure 10.1: Circuit for the adder program adapted from [15]. Duration (s) 50 qubits 75 qubits 100 qubits 125 qubits 150 qubits 175 qubits 200 qubits CVC5 4 24 71 171 365 751 1069 Bitwuzla 3 12 29 98 158 248 313 [PITH_FULL_IMAGE:figures/full_fig_p019_10_1.png]

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

47 extracted references · 21 canonical work pages

  1. [1]

    Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al . 2022. cvc5: A versatile and industrial-strength SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 415–442

    work page 2022

  2. [2]

    Bennett, Richard Cleve, David P

    Adriano Barenco, Charles H. Bennett, Richard Cleve, David P. Di- Vincenzo, Norman Margolus, Peter Shor, Tycho Sleator, John A. Smolin, and Harald Weinfurter. 1995. Elementary gates for quan- tum computation. Phys. Rev. A 52 (Nov 1995), 3457–3467. Issue 5. https://doi.org/10.1103/PhysRevA.52.3457

    doi:10.1103/physreva.52.3457 1995

  3. [3]

    Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev

    work page

  4. [4]

    Bradben and geduardo. 2024. Quantum Memory Management in Q#. https://learn.microsoft.com/en-us/azure/quantum/user-guide/ language/statements/quantummemorymanagement

    work page 2024

  5. [5]

    Cirq Developers. 2023. Cirq. https://doi.org/10.5281/zenodo.8161252

    doi:10.5281/zenodo.8161252 2023

  6. [6]

    Bishop, Steven Heidel, Colm A

    Andrew Cross, Ali Javadi-Abhari, Thomas Alexander, Niel De Beau- drap, Lev S. Bishop, Steven Heidel, Colm A. Ryan, Prasahnt Sivarajah, John Smolin, Jay M. Gambetta, and Blake R. Johnson. 2022. OpenQASM 3: A Broader and Deeper Quantum Assembly Language. ACM Trans- actions on Quantum Computing 3, 3, Article 12 (Sept. 2022), 50 pages. https://doi.org/10.1145/3505636

    doi:10.1145/3505636 2022

  7. [7]

    Cuccaro, Thomas G

    Steven A. Cuccaro, Thomas G. Draper, Samuel A. Kutin, and David Petrie Moulton. 2004. A new quantum ripple-carry addition cir- cuit. arXiv:quant-ph/0410184 [quant-ph] https://arxiv.org/abs/quant- ph/0410184

    arXiv 2004

  8. [8]

    Tannu, Prashant J

    Poulami Das, Swamit S. Tannu, Prashant J. Nair, and Moinuddin Qureshi. 2019. A Case for Multi-Programming Quantum Computers. In Proceedings of the 52nd Annual IEEE/ACM International Sympo- sium on Microarchitecture (Columbus, OH, USA) (MICRO ’52) . As- sociation for Computing Machinery, New York, NY, USA, 291–303. https://doi.org/10.1145/3352460.3358287

    arXiv 2019

Show all 47 references
  1. [9]

    Thomas G. Draper. 2000. Addition on a Quantum Computer. arXiv:quant-ph/0008033 [quant-ph] https://arxiv.org/abs/quant-ph/ 0008033

    2000 arXiv

  2. [10]

    Yuan Feng and Yingte Xu. 2023. Verification of nondeterministic quan- tum programs. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3. 789–805

    2023

  3. [11]

    Craig Gidney. 2015. Constructing Large Controlled Nots. https://algassert.com/circuits/2015/06/05/Constructing-Large- Controlled-Nots.html Accessed: 2025-08-02

    2015

  4. [12]

    Craig Gidney. 2018. Factoring with n+2 clean qubits and n-1 dirty qubits. arXiv:1706.07884 [quant-ph] https://arxiv.org/abs/1706.07884

    2018 arXiv

  5. [13]

    Alexandre Goy and Daniela Petrişan. 2020. Combining probabilistic and non-deterministic choice via weak distributive laws. InProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science . 454–464

    2020

  6. [14]

    Green, Peter LeFanu Lumsdaine, Neil J

    Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. 2013. Quipper: a scalable quantum pro- gramming language. In Proceedings of the 34th ACM SIGPLAN Confer- ence on Programming Language Design and Implementation (Seattle, Washington, U...

    2013 doi

  7. [15]

    Thomas Häner, Martin Roetteler, and Krysta M Svore. 2017. Factoring using 2n+2 qubits with toffoli based modular multiplication. Quantum Information & Computation 17, 7-8 (2017), 673–684. 12 Borrowing Dirty Qubits in Quantum Programs

    2017

  8. [16]

    Zhenyu Huang, Fuxin Zhang, and Dongdai Lin. 2025. Constructing Quantum Implementations with the Minimal T-depth or Minimal Width and Their Applications. In Advances in Cryptology – EURO- CRYPT 2025: 44th Annual International Conference on the Theory and Applications of Cryptog...

    2025 doi

  9. [17]

    Hanru Jiang. 2024. Qubit Recycling Revisited. 8, PLDI, Article 198 (June 2024), 24 pages. https://doi.org/10.1145/3656428

    2024 doi

  10. [18]

    Yangjia Li and Mingsheng Ying. 2017. Algorithmic analysis of termi- nation problems for quantum programs. Proc. ACM Program. Lang. 2, POPL, Article 35 (Dec. 2017), 29 pages.https://doi.org/10.1145/3158123

    2017 doi

  11. [19]

    Lei Liu and Xinglei Dou. 2021. QuCloud: A New Qubit Mapping Mech- anism for Multi-programming Quantum Computing in Cloud Envi- ronment. In 2021 IEEE International Symposium on High-Performance Computer Architecture (HPCA) . 167–178. https://doi.org/10.1109/ HPCA51647.2021.00024

    2021

  12. [20]

    Lei Liu and Xinglei Dou. 2024. QuCloud+: A Holistic Qubit Map- ping Scheme for Single/Multi-programming on 2D/3D NISQ Quan- tum Computers. 21, 1, Article 9 (Jan. 2024), 27 pages. https: //doi.org/10.1145/3631525

    2024 doi

  13. [21]

    Guang Hao Low, Vadym Kliuchnikov, and Luke Schaeffer. 2024. Trad- ing T gates for dirty qubits in state preparation and unitary synthesis. Quantum 8 (June 2024), 1375. https://doi.org/10.22331/q-2024-06-17- 1375

    2024 doi

  14. [22]

    Aina Niemetz and Mathias Preiner. 2023. Bitwuzla. In Computer Aided Verification - 35th International Conference, CA V 2023, Paris, France, July 17-22, 2023, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 13965), Constantin Enea and Akash Lal (Eds.). Springer, 3...

    2023 doi

  15. [23]

    Anouk Paradis, Benjamin Bichsel, Samuel Steffen, and Martin Vechev

  16. [24]

    Anouk Paradis, Benjamin Bichsel, and Martin Vechev. 2024. Reqomp: Space-constrained Uncomputation for Quantum Circuits. Quantum 8 (Feb. 2024), 1258. https://doi.org/10.22331/q-2024-02-19-1258

    2024 doi

  17. [25]

    Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: a core language for quantum circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL ’17). Association for Computing Machinery, New York, NY, USA, 846...

    2017

  18. [26]

    John Preskill. 2018. Quantum Computing in the NISQ era and beyond. Quantum 2 (Aug. 2018), 79. https://doi.org/10.22331/q-2018-08-06-79

    2018 doi

  19. [27]

    John Preskill. 2025. Beyond NISQ: The Megaquop Machine. ACM Transactions on Quantum Computing (March 2025). https://doi.org/ 10.1145/3723153 Just Accepted

    2025 doi

  20. [28]

    Qiskit contributors. 2023. Qiskit: An Open-source Framework for Quantum Computing. https://doi.org/10.5281/zenodo.2573505

    2023 doi

  21. [29]

    Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic

  22. [30]

    Raphael Seidel, Nikolay Tcholtchev, Sebastian Bock, and Manfred Hauswirth. 2023. Uncomputation in the Qrisp High-Level Quantum Programming Framework. In Reversible Computation, Martin Kutrib and Uwe Meyer (Eds.). Springer Nature Switzerland, Cham, 150–165

    2023

  23. [31]

    Peter Selinger. 2004. Towards a quantum programming language. Mathematical Structures in Computer Science 14, 4 (2004), 527–586. https://doi.org/10.1017/S0960129504004256

    2004 doi

  24. [32]

    Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, An- dres Paz, and Martin Roetteler. 2018. Q#: Enabling Scalable Quantum Computing and Development with a High-level DSL. InProceedings of the Real...

    2018

  25. [33]

    Yasuhiro Takahashi, Seiichiro Tani, and Noboru Kunihiro. 2010. Quan- tum addition circuits and unbounded fan-out. Quantum Information and Computation 10, 9-10 (2010), 872–890

    2010

  26. [34]

    Hristo Venev, Timon Gehr, Dimitar Dimitrov, and Martin Vechev

  27. [35]

    Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks. 2023. Qunity: A Unified Language for Quantum and Classical Computing. 7, POPL, Article 32 (jan 2023), 31 pages. https://doi.org/10.1145/3571225

    2023 doi

  28. [36]

    Dave Wecker and Krysta M. Svore. 2014. LIQUi|>: A Software Design Architecture and Domain-Specific Language for Quantum Computing. arXiv:1402.4467 [quant-ph] https://arxiv.org/abs/1402.4467

    2014 arXiv

  29. [37]

    Ming Xu, Jianling Fu, Hui Jiang, Yuxin Deng, and Zhi-Bin Li. 2024. Termination and Universal Termination Problems for Nondeterminis- tic Quantum Programs. ACM Trans. Softw. Eng. Methodol. 33, 8, Article 219 (Dec. 2024), 41 pages. https://doi.org/10.1145/3691632

    2024 doi

  30. [38]

    Mingsheng Ying. 2012. Floyd–hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33, 6, Article 19 (jan 2012), 49 pages. https://doi.org/10.1145/2049706.2049708

    2012

  31. [39]

    Mingsheng Ying. 2024. Foundations of Quantum Programming (2nd Edotion). Morgan Kaufmann. 13 Bonan Su, Li Zhou, Yuan Feng, and Mingsheng Ying 9 Deferred Proofs 9.1 Proof of Theorem 5.3 Theorem 9.1. A program𝑆 safely uncomputes a qubit 𝑞 if and only if for all states 𝜌 and any o...

    2024

  32. [44]

    In addition, we strengthen the induction hypothesis by requiring not only that| J𝑆K| = 1, but also that J𝑆K acts as identity on qubits other than𝑞𝑢𝑏𝑖𝑡𝑠(𝑆). The base case is when𝑆≡ skip,[𝑞] :=|0⟩ or𝑈[ ¯𝑞], by the denotational semantics given in Figure 4.3, it trivially holds th...

  33. [45]

    𝑆 safely uncomputes𝑞

  34. [46]

    (5.1) holds for every|𝜓⟩∈{| 0⟩,|1⟩,|+⟩,|+𝑖⟩,|−⟩} and every state𝜌∈{ 𝜌′⊗|𝜓⟩𝑞⟨𝜓| :𝜌′∈ ℬ⊗( 𝑛−1)}

  35. [47]

    (5.2) holds for one additional hypothetical qubit ¯𝑞′ =𝑞′, the Bell state 𝜌′ = |Φ⟩⟨Φ|, and for every state 𝜌 ∈ {𝜌′⊗| Φ⟩𝑞,𝑞′⟨Φ| :𝜌′∈ ℬ⊗( 𝑛−2)}. Proof. (1 =⇒ 2) Similar to the proof of (⇒) direction in Theorem 5.3. (2 =⇒ 1) Let H = ∯ 𝑞′∈qubits\{𝑞}H𝑞′. Given that ℬ⊗( 𝑛−1) forms a...

  36. [2019]

    Elec- tronic Proceedings in Theoretical Computer Science 287 (Jan

    ReQWIRE: Reasoning about Reversible Quantum Circuits. Elec- tronic Proceedings in Theoretical Computer Science 287 (Jan. 2019), 299–312. https://doi.org/10.4204/eptcs.287.17

    2019 doi

  37. [2020]

    In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (London, UK) (PLDI 2020)

    Silq: a high-level quantum language with safe uncomputation and intuitive semantics. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (London, UK) (PLDI 2020). Association for Computing Machinery, New York, NY, USA, 286–300. h...

    2020

  38. [2021]

    In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

    Unqomp: synthesizing uncomputation in Quantum circuits. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation . 222–236

  39. [2024]

    Modular Synthesis of Efficient Quantum Uncomputation. Proc. ACM Program. Lang. 8, OOPSLA2, Article 345 (Oct. 2024), 28 pages. https://doi.org/10.1145/3689785

    2024 doi

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.