ReOC: Compilation of Recursive Quantum Oracles with Recursion-Aware Uncomputation

Huiling Wu; Yuxin Deng

REVIEW 4 major objections 4 minor 39 references

ReOC: Compilation of Recursive Quantum Oracles with Recursion-Aware Uncomputation

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

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

Pith's one-line read This paper presents a compiler that turns classical-style recursive oracle specifications into reversible quantum programs with provably correct, recursion-aware uncomputation.

desk verdict Promising design for compiling recursive quantum oracles, but the main correctness theorem doesn't cover the program the compiler actually runs. read the letter →

arxiv 2608.07973 v1 pith:MIETHTBX submitted 2026-08-08 cs.PL

Huiling Wu , Yuxin Deng This is my paper · ORCID

classification cs.PL

keywords quantumoraclesreversiblecompilationrecursiveprogramscontrolflowuncomputationRQIMPRQC++registerreuse

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 claims that recursive quantum oracles—programs whose recursion path depends on quantum data in superposition—can be written in a classical-style imperative language and compiled automatically into reversible quantum programs. The compiler, ReOC, translates the source language RQIMP into RQC++, an existing quantum language with quantum control flow, and takes over the two tasks that make manual RQC++ programming hard: isolating quantum registers across recursion layers and uncomputing temporary variables. Its indexed static-register discipline turns live variables into indexed registers that each recursive call increments, so layers never collide, while its recursion-aware cleanup defers uncomputation of recursive-call temporaries (avoiding exponential recomputation) and eagerly cleans other temporaries (controlling space). For linear recursion the paper proves time and space overhead linear in recursion depth. The central result, Theorem 6.2, is a mathematical proof that every well-typed RQIMP program and its compiled target are semantically equivalent, with all temporary quantum variables correctly restored.

What carries the argument

The machinery is a compilation pipeline with three load-bearing components. RQIMP, the source language, is a typed imperative language with C/Q modes; its type system enforces single assignment, forbids non-main functions from modifying globals, and keeps globals read-only or write-only in main, all of which the correctness proof needs so that target procedures are well-formed and cleanup is reversible. The indexed static-register discipline is the storage mechanism: an index supplier $\iota$ issues index variables, live quantum variables are rewritten as subscripted registers of the form $q[i]$, recursive calls pass $i+1$ so successive layers touch disjoint slots, and independent index variables are assigned to distinct recursive paths; variables already cleaned stay unsubscripted and are reused. The variable dependency graph is the cleanup scheduler: each variable node carries a flag (0 for eager cleanup of non-recursive temporaries, 1 for end-of-layer cleanup in non-linear recursion, 2 for cleanup postponed to the outermost call in linear recursion), mutually dependent variables are merged into composite nodes cleaned as a unit, and each node stores a cleanup circuit whose inverse restores it to $|0\rangle$. On top of these, Theorem 6.2 states the main claim: for every well-typed RQIMP program, Compile_Prog yields a target with $C_{\mathrm{main}} \approx s_{\mathrm{main}}$, proved by relating $k$-th syntactic approximations of the two programs.

What would settle it

Take a well-typed RQIMP program (for instance the sum oracle), run its compiled RQC++ target through the QRM backend on every basis input, and check that each temporary annotated for cleanup returns to $|0\rangle$ after execution and that for linear recursion the number of recursive invocations grows linearly with input depth; any residual entanglement of temporaries, any violation of RQC++'s well-formedness conditions in a generated declaration, or an exponential invocation count would refute Theorem 6.2 or the linear-overhead claim.

Watch

Extended reading notes

Core claim

A programmer writes a recursive oracle in RQIMP—with quantum-mode guards, loops, and mutual recursion—and the compiler returns an RQC++ program whose observable behavior matches the source on every input. The paper's correctness statement is semantic equivalence between the target and source main procedures: for every initial source state, the two programs either both diverge or both terminate with the encoded result, and every auxiliary quantum register ends in $|0\rangle$. The proof works by compiling under a live-variable discipline: at each recursive call the compiler converts the caller's live quantum variables into subscripted form with incremented indices, guaranteeing disjoint register slots per layer, and it annotates each temporary with a cleanup flag that decides whether uncomputation is eager (non-recursive statements), deferred to the end of a layer (non-linear recursion), or deferred to the outermost call (linear recursion). The running example is the sum oracle, whose naive per-layer uncomputation would recompute the recursive subcall at every layer and grow exponentially; the compiled target defers cleanup of those temporaries to the top level and keeps the invocation count linear.

Load-bearing premise

All compiled programs live in an extension of RQC++ that permits quantum variables as call-by-reference procedure parameters; the paper argues this reduces to passing classical address and index data for statically allocated storage, but does not itself prove that the extension is sound or that the QRM backend realizes it, so the correctness theorem is only as strong as that unproved reduction.

Editorial extensions

If this is right

Programmers can specify recursive oracles (recursive summation, exponentiation by squaring, union-find find, depth-first search) in a classical structured style and receive reversible RQC++ code, with register indexing and uncomputation generated automatically rather than hand-written.
For linear recursion the generated program runs with invocation overhead linear in recursion depth and additional space $O(n(K+1)+N+M)$ for depth $n$ and per-layer register counts $K,N,M$, so the exponential recomputation of naive per-layer cleanup is avoided.
Because the compiled main procedure leaves every auxiliary register in $|0\rangle$, the generated oracle can be invoked inside larger quantum algorithms and cleaned up by executing the inverse of the whole call, without leaking temporary garbage into the output.
The generated targets inherit the existing RQC++-to-QRM compilation chain, giving an executable route from a high-level recursive specification to a quantum register machine with quantum control flow and recursive procedure calls.
Well-typed RQIMP programs are guaranteed by the proof to compile to semantically equivalent targets, so type checking the source takes the place of debugging index management and cleanup timing in the target.

Reading between the lines

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

The selective-cleanup recipe (defer only recursive-call temporaries, eagerly clean everything else, index only live variables) is a general design principle that could be adopted by other quantum languages with automatic uncomputation, even outside the RQC++/QRM setting; the paper itself does not claim this transfer.
The paper proves its linear-overhead bound as a per-layer accounting argument but lists an implementation as future work, so the natural test of the resource claims is to build the pipeline on the QRM backend and measure invocation counts and register footprints for the sum, power, find, and DFS examples; that measurement does not yet exist.
The paper's own case study notes that its per-layer cleanup for non-linear recursion can still risk exponential time in branch-heavy recursion such as DFS on a chain; a cost-model-driven policy that picks cleanup timing per call site from the dependency graph would be a concrete next step beyond this paper.
The correctness proof is mathematical rather than machine-checked and lives in a language extension (quantum call-by-reference parameters) whose reduction to classical address and index passing is argued rather than formally proved; a mechanized proof of the same theorem, or a proof that the extension is conservative over RQC++, would close the remaining gap.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

Here's my take: the design is promising, but the correctness theorem has a gap the authors should fix. The direction—compiling recursive oracles with quantum control flow from a structured source language into RQC++—is genuinely useful, and the two core techniques (indexed static-register isolation, flag-based uncomputation) are sensible. The linear-recursion overhead argument is plausible, and the case studies (sum, union-find, DFS) show the intended scope.

The main soft spot is that Theorem 6.2 is stated for well-typed RQIMP programs, but the compiler first applies high-level transformations that the paper's own Appendix D.1 says 'temporarily relax' the type system. In particular, branch extraction for C-mode conditionals can generate procedures that return C-mode variables, which the RQIMP type system forbids. The paper says these calls can be inlined afterwards, but the compilation pipeline compiles the transformed program directly, with no inlining pass before Compile_Prog. So the actual input to the compiler may be outside the well-typed fragment for which the type-soundness lemmas and the proof of Theorem 6.2 are established. That's a real mismatch between the theorem's hypothesis and the compiler's behavior. It looks fixable—either by extending the correctness proof to the relaxed grammar, or by inserting the promised inlining pass—but as written the proof doesn't cover the program that actually gets compiled.

There's a second issue: the main proof is a sketch, with key lemmas (F.19, F.62, etc.) deferred to an appendix that wasn't in the review copy. For a PL paper, that is a serious handicap. I can't verify the central claim from the main text, and that makes the correctness result conditional. The paper is otherwise honest about its limitations: it lists machine-checked verification as future work, and the case studies include explicit caveats about the DFS cleanup. The resource analysis is parameterized, not overclaiming.

Who should read it: people working on quantum control flow and reversible compilation, particularly recursion and uncomputation. The paper deserves a serious referee rather than a desk reject, but I'd expect major revision: complete the proof, resolve the type-system mismatch, and ideally add an implementation or machine-checked key lemmas before it's publishable.

Referee Report

4 major / 4 minor

Summary. The paper presents ReOC, a compilation framework that translates programs in a new imperative source language RQIMP into recursive quantum programs in RQC++, with the goal of supporting quantum-controlled recursive oracles. The compiler uses an indexed static-register discipline to isolate live quantum variables across recursion layers and a recursion-aware uncomputation strategy that defers cleanup of recursive-call temporaries while cleaning non-recursive temporaries eagerly. The paper claims a semantic-preservation theorem (Theorem 6.2) covering termination equivalence, output correspondence, and correct uncomputation, as well as linear recursion-depth overhead for linear recursion in Section 4.

Significance. If the main claims hold, this addresses a genuine gap in quantum oracle compilation: structured high-level specifications of recursively defined oracles with quantum-dependent control flow, compiled to a target language with existing backend support. The paper is honest about its scope, makes no empirical claims, and avoids fitted parameters; the resource analysis is explicitly parameterized by per-layer costs, and the correctness statement includes uncomputation of temporary variables, which is a strong and falsifiable claim. The main value is conceptual: separating shareable from non-shareable registers and choosing cleanup timing by variable origin is a plausible and reusable design. However, the significance is conditional on closing the gap between the theorem's hypotheses and the compiler's actual input, and on providing the deferred proofs.

major comments (4)

[Section 5.1, Appendix D.1, Theorem 6.2] There is a load-bearing mismatch between the correctness theorem and the program actually compiled. Theorem 6.2 is stated for every well-typed RQIMP program, but the compilation pipeline in Figure 9 and Algorithm 1 first applies high-level transformations and then compiles the transformed program directly, with no separate inlining pass before Compile_Prog. Appendix D.1 explicitly says that C-mode conditionals are turned into non-recursive function calls that may return classical variables, even though the function-declaration rule in Table 7 restricts return values to Q-mode; the remark that such calls "can be inlined afterwards" is not reflected in the described pipeline. Since the type-soundness theorems in Section 3.4 and the typing-based invariants used in Section 5.6 (e.g., that mvq(s) is written for the first time) are proved for the original grammar, the paper does not establish that the input to the compiler satisfies the hypotheses of Theorem 6.2.
[Appendix B, Section 4] The target-language extension is not given a precise semantics. Every generated target program uses quantum variables as procedure parameters, but the formal operational semantics of RQC++ in Appendix B.3, especially rule (RC), substitutes formal parameters inside "begin local u:=t; C end" and rule (AS) assigns only classical expressions to classical variables. The paper's call-by-reference justification is an informal argument about compiling quantum arguments to classical address/index information, not a conservative-extension theorem for the defined semantics. Consequently, the statement that C_main is an RQC++ program whose semantics is covered by Theorem 6.2 is not well defined until this extension is formalized or shown to be an abbreviation of the original language.
[Section 4, Section 6] The advertised resource guarantee for linear recursion is not proved. The text asserts that additional space is bounded by (N+(n-1)K)+n+M and that time overhead is linear in recursion depth parameterized by per-layer costs, but N, K, and M are described only informally and no theorem in Section 6 or in the appendices states or proves such a bound in terms of the compilation algorithms of Section 5. Theorem 6.2 is purely a semantic equivalence theorem and contains no complexity clause. The authors should either state and prove a formal resource theorem or explicitly label the Section 4 analysis as heuristic rather than a contribution.
[Appendix F] The detailed proof of the central correctness claim is not available for verification. The proof sketch of Theorem 6.2 depends on Theorem F.19, Lemma F.62, and the arguments in Appendix F.7, but the submitted Appendix F ends inside the notation section F.1, so these statements are never given. As received, the manuscript's main soundness claim rests on lemmas that the reader cannot check. The full appendix should be included, and the key lemmas on which the main theorem depends should be stated in the main text.

minor comments (4)

[Figure 14] The RQC++ program in Figure 14 shows "Fsum(p1,r1,0));" with an unbalanced parenthesis; this should be corrected for consistency with the indexed call in Figure 4.
[Section 6] The encoding E(σ,ρ) is written as a pair containing σ_c, but the text then says "we omit σ_c and focus solely on the quantum part"; the treatment of classical-mode variables in the target-state correspondence should be made explicit, otherwise the equality in the definition of ≈ is ambiguous.
[Table 3, Section 3.1] The typing rule for "for" loops in Table 3 requires the loop variable and bound to be in Q-mode, while Section 3.1 says that loops depending only on classical data are compiled by unrolling; the paper should clarify how classical loops are typed before the high-level transformations are applied.
[Section 4, Section 5.2] The flag values 0, 1, 2 are introduced in Section 4 as cleanup-timing annotations but are formally attached to variable nodes only later in Section 5.2, where the relationship between a variable's flag and the flag of its composite node is defined; consolidating these definitions would avoid the impression that the meaning of the flag shifts between 'origin of the variable' and 'cleanup timing'.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the compiler-correctness proof is self-contained and no predicted quantity reduces to an input by construction.

full rationale

The paper's central claim (Theorem 6.2) is a compiler-correctness theorem proved by induction over finite syntactic approximations of both source and target programs. There are no fitted constants, no empirical predictions, and no parameter that is first fit to data and then reported as a prediction. The resource-overhead claims for linear recursion are derived directly from the described indexed static-register and deferred-uncomputation algorithms, parameterized by per-layer register footprint and primitive-operation costs, so they are consequences of the algorithm rather than inputs to it. The extension of RQC++ to allow quantum variables as call-by-reference parameters is justified by an explicit reduction to classical address/index information for statically allocated quantum storage; this is an argument about realizability, not an assumption of the correctness theorem. The only internal-looking dependency is the use of the paper's own appendices and lemmas in the proof of Theorem 6.2, which is normal proof structure rather than circularity. The skeptical concern that the high-level transformations in Appendix D.1 temporarily relax the RQIMP type system, potentially putting the compiler's actual input outside the well-typed fragment covered by Theorem 6.2, is a correctness and coverage risk, not a circularity: even if the theorem's hypothesis does not match the transformed program, that would be an unsupported proof obligation, not an equation that reduces the conclusion to the premise. No specific circular step can be exhibited from the text, so the appropriate finding is no significant circularity.

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

The central claims rest on no fitted parameters: the resource bounds use symbolic per-layer quantities K, N, M and the machine word size sz, which are structural inputs rather than numbers tuned to data. The uncomputation strategy and indexed-register discipline are justified by the paper's own construction, not by fitting. The axioms collected here are the unproved or externally delegated background facts the correctness theorem depends on, most notably the soundness of the RQC++ extension with quantum parameters, the finite-unfolding adequacy of the target semantics, and the QRM backend's ability to realize indexed storage within a finite execution bound. The RQIMP language and the extended RQC++ are new artifacts introduced by the paper; neither has an outside-paper validation, so both are listed as invented entities with independent_evidence false.

assumptions (5)

domain assumption Finite-unfolding adequacy: a recursive RQIMP or RQC++ program terminates with a result iff some finite syntactic approximant terminates with the same result.
Invoked without proof in the proof of Theorem 6.2 (Section 6) to relate source termination, target termination, and approximants.
domain assumption RQC++ with the paper's extension to quantum procedure parameters is a well-defined deterministic language with the operational semantics of Appendix B.
The compilation targets this extended language; the soundness of the extension is argued in Appendix B by reduction to classical index passing, but not formally proved.
domain assumption The QRM backend can realize the indexed static-storage discipline within finite QRAM layout, including the finite execution bound T_exe and timeout behavior.
Stated in Appendix D under 'Finite storage interpretation of indexed variables'; correctness of the low-level realization is delegated to the cited QRM backend.
ad hoc to paper High-level transformations preserve source semantics and map into the fragment covered by the correctness proof, or the correctness proof covers the relaxed type system.
Section 5.1 claims the transformed program stays in RQIMP, but Appendix D.1 admits a temporary relaxation of the type system and procedures returning classical variables; the paper does not show the relaxation is covered by Theorem 6.2.
domain assumption QFT-based arithmetic oracles from VQO are correct and reusable as primitive operations.
Section 5.5 states arithmetic operations are implemented using QFT-based methods from VQO; correctness of the compiled circuits depends on these primitives.

invented entities (2)

RQIMP language
purpose: High-level imperative source language for recursive oracles with quantum control flow.
Section 3 introduces RQIMP; its usability rests on compilation theorems whose full proofs are deferred to Appendix F, and its transformed fragment relaxes the type system, so there is no outside-paper validation such as a reference implementation or machine-checked metatheory.
Quantum variables as procedure parameters in RQC++ (call-by-reference extension)
purpose: Allow compiled procedures to operate on different quantum registers across recursion layers.
Appendix B argues the extension is a syntactic convenience reducible to classical index arguments, but the argument is informal and the entire compiled output is expressed in this extended language.

how reviews work

0 comments

Cite this review

Pith. "Pith review of ReOC: Compilation of Recursive Quantum Oracles with Recursion-Aware Uncomputation." pith.science (2026). https://pith.science/paper/MIETHTBX

@misc{pith2026260807973,
  author       = {Pith},
  title        = {Pith review of: ReOC: Compilation of Recursive Quantum Oracles with Recursion-Aware Uncomputation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MIETHTBX}},
  note         = {Machine review of arXiv:2608.07973}
}

read the original abstract

Quantum oracles are essential to many quantum algorithms, and their specifications may involve recursive control flow that depends on runtime quantum data. However, existing reversible compilation frameworks provide limited support for such quantum-controlled recursive structures. We present ReOC, a compilation framework that transforms high-level recursive oracle specifications with quantum control flow into reversible quantum programs. The framework comprises RQIMP, a high-level imperative source language for specifying recursive oracles, and a method of compiling programs in that language into RQC++, an existing high-level quantum recursive language with quantum control flow. In this way, we avoid the tedious and error-prone process of directly writing quantum oracles in RQC++. To manage static storage under dynamic quantum control, ReOC uses an indexed static-register discipline to isolate live variables across recursion layers, enabling safe register reuse while controlling quantum storage usage. Furthermore, to address the exponential time blow-up caused by naive uncomputation in recursive settings, ReOC employs a recursion-aware uncomputation strategy: temporary variables from recursive calls are cleaned using deferred strategies to control time overhead, while those from non-recursive statements are cleaned eagerly to reduce space usage. For linear recursion, this strategy yields overhead linear in recursion depth, parameterized by the per-layer register footprint and primitive-operation costs. Finally, we provide a mathematical proof of compilation correctness from RQIMP to RQC++, establishing semantic preservation and correct uncomputation of temporary quantum variables.

Figures

Figures reproduced from arXiv: 2608.07973 by the authors.

**Figure 3.** RQC++ sum: incorrect use of temporaries. 1 Fsum(p,r,i) ⇐= 2 circ(k==0, q[i]); 3 qif q[i]( 4 |0> -> circ(k-1, q1[i]); 5 Fsum(q1[i],q2[i],i + 1); 6 qinv(circ(k-1, q1[i])); // Uncompute q1[i] 7 circ(k+y, r); 8 qinv(Fsum(q1[i],q2[i],i + 1)) // Uncompute q2[i] 9 □ |1> -> circ(0, r) ); 10 qinv(circ(k==0, q[i])) // Uncompute q[i] 11 fiq [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗

**Figure 5.** A diagram depicting a mutual recursion example: nodes represent function names or call sites, solid [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗

Figures from the paper (22 more)

**Figure 7.** Figure 7: The target program of sum. integrated unit, keep those variables live across recursion layers until the top-level call finishes, and then uncompute them uniformly. For example, in [PITH_FULL_IMAGE:figures/full_fig_p013_7.png]

**Figure 8.** Figure 8: Source and target programs of f1. For more complex non-linear recursive structures, deferring all ancillae for recursive calls until the top level may lead to space explosion. For these cases, we perform cleanup in each layer to mitigate this issue. In particular, we …

**Figure 9.** Figure 9: The compilation process. In this section, we show how to compile an RQIMP program 𝑃 into RQC++ using the key techniques described above [PITH_FULL_IMAGE:figures/full_fig_p014_9.png]

**Figure 10.** Figure 10: Structure of the compilation algorithms. Internally, Compile_Body compiles the statements of the function body inductively into the corresponding RQC++ program. As shown in [PITH_FULL_IMAGE:figures/full_fig_p017_10.png]

**Figure 11.** Figure 11: The Workflow for Compilation of Functions. The function-compilation algorithm Compile_Fun compiles a function 𝑓 by operating on the compilation context ctx. It proceeds in seven steps, as shown in [PITH_FULL_IMAGE:figures/full_fig_p018_11.png]

**Figure 12.** Figure 12: The workflow for compilation of function bodies The algorithm first invokes Compile_Com to generate the target circuit 𝐶𝑠 for statement 𝑠 and then updates the cleanup circuits of the relevant nodes in 𝜅. For instance, if the statement 𝑠 is not a linear recursive ca…

**Figure 13.** Figure 13: The workflow for the uncomputation of temporary quantum variables. Step 2. The inserted uncomputation circuit restores each variable 𝑦 in 𝑤 with 𝑦.flag ≠ 2 to its initial value. Therefore, for each such source variable that is not an input parameter, meaning that the…

**Figure 14.** Figure 14: The full RQC++ program for sum (enlarged version of [PITH_FULL_IMAGE:figures/full_fig_p029_14.png]

**Figure 15.** Figure 15: Quantum variables of RQC++ commands B.2 Syntax A program is a set D of procedure declarations of the form 𝑃 (𝑢) ⇐ 𝐶, where 𝑢 = 𝑢1, . . . , 𝑢𝑛 is a list of formal parameters (classical simple variables) and 𝐶 is a statement (the procedure body). One procedure, say 𝑃mai…

**Figure 16.** Figure 16: Inverse transformation of RQC++ commands The justification of this extension is that once the program is compiled, all quantum variables (including array elements) can be statically allocated into a large multi-dimensional quantum storage space, where each variable na…

**Figure 17.** Figure 17: Transition rules for the operational semantics of [PITH_FULL_IMAGE:figures/full_fig_p032_17.png]

**Figure 18.** Figure 18: Selected Proof Rules for Program Constructs [PITH_FULL_IMAGE:figures/full_fig_p034_18.png]

**Figure 19.** Figure 19: Dependency subgraphs for statement types. [PITH_FULL_IMAGE:figures/full_fig_p039_19.png]

**Figure 20.** Figure 20: Quantum program implementing recursive exponentiation [PITH_FULL_IMAGE:figures/full_fig_p058_20.png]

**Figure 21.** Figure 21: The source and target procedures implementing the find operation [PITH_FULL_IMAGE:figures/full_fig_p059_21.png]

**Figure 22.** Figure 22: The source and target procedures implementing DFS [PITH_FULL_IMAGE:figures/full_fig_p060_22.png]

**Figure 23.** Figure 23: Proof dependencies for the correctness of Clean_Temp; arrows point from a result to the lemmas or [PITH_FULL_IMAGE:figures/full_fig_p073_23.png]

**Figure 24.** Figure 24: Transformation of the Clean Variable Pool in the [PITH_FULL_IMAGE:figures/full_fig_p076_24.png]

**Figure 25.** Figure 25: Proof dependencies for the correctness of [PITH_FULL_IMAGE:figures/full_fig_p088_25.png]

**Figure 26.** Figure 26: Proof dependencies for the correctness of [PITH_FULL_IMAGE:figures/full_fig_p098_26.png]

**Figure 27.** Figure 27: Proof dependencies for the correctness of [PITH_FULL_IMAGE:figures/full_fig_p121_27.png]

**Figure 28.** Figure 28: Transformation of the clean variable pool [PITH_FULL_IMAGE:figures/full_fig_p125_28.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

39 extracted references · 15 canonical work pages

[1]

Abhari, Arvin I

Ali J. Abhari, Arvin I. Faruque, Mohammad Javad Dousti, Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, and Fred Chong. 2012.Scaffold: Quantum Programming Language. Technical Report. Princeton University. https://api.semanticscholar.org/CorpusID:18354908

work page 2012
[2]

Andris Ambainis, Kaspars Balodis, J ¯anis Iraids, Martins Kokainis, Krišj ¯anis Pr ¯usis, and Jevg ¯enijs Vihrovs. 2018. Quantum Speedups for Exponential-Time Dynamic Programming Algorithms. doi:10.48550/arXiv.1807.05209 arXiv:1807.05209 [quant-ph]

work page Pith review arXiv doi:10.48550/arxiv.1807.05209 2018
[3]

Matthew Amy, Martin Roetteler, and Krysta M. Svore. 2017. Verified Compilation of Space-Efficient Reversible Circuits. InComputer Aided Verification - 29th International Conference, CA V 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II (Lecture Notes in Computer Science), Rupak Majumdar and Viktor Kuncak (Eds.). Springer, 3–21. doi:10.100...

work page doi:10.1007/978-3-319-63390-9_1 2017
[4]

C. H. Bennett. 1973. Logical reversibility of computation.IBM J. Res. Dev.17, 6 (Nov. 1973), 525–532. doi:10.1147/rd. 176.0525

doi:10.1147/rd 1973
[5]

Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. 2020. Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics. InProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, London UK, 286–300. doi:10.1145/3385412.3386007

arXiv 2020
[6]

Yongshan Ding, Xin-Chuan Wu, Adam Holmes, Ash Wiseth, Diana Franklin, Margaret Martonosi, and Frederic T. Chong
[7]

Christoph Durr, Mark Heiligman, Peter Hoyer, and Mehdi Mhalla. 2006. Quantum Query Complexity of Some Graph Problems.SIAM J. Comput.35, 6 (Jan. 2006), 1310–1328. doi:10.1137/050644719 arXiv:quant-ph/0401091

work page Pith review arXiv 2006
[8]

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 programming language. InProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation(Seattle, Washington, USA)(PLDI ’13). Association for Computing Machinery, New York, NY, USA, 333–342. doi:10...

arXiv 2013

Show all 39 references

[9]

Lov K. Grover. 1996. A fast quantum mechanical algorithm for database search. InProceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing(Philadelphia, Pennsylvania, USA)(STOC ’96). Association for Computing Machinery, New York, NY, USA, 212–219. doi:10.1145...

1996
[10]

Kengo Hirata and Chris Heunen. 2025. Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime. Proc. ACM Program. Lang.9, POPL (Jan. 2025), 6:155–6:182. doi:10.1145/3704842 ReOC: Compilation of Recursive Quantum Oracles with Recursion-Aware Uncomputation 27

2025 doi
[11]

Vladislavs Kl,evickis, Krišj¯anis Pr¯usis, and Jevg¯enijs Vihrovs. 2022. Quantum Speedups for Treewidth. In17th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2022) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 232), Fra...

2022 doi
[12]

Tanuj Khattar and Craig Gidney. 2025. Rise of Conditionally Clean Ancillae for Efficient Quantum Circuit Constructions. Quantum9 (May 2025), 1752. doi:10.22331/q-2025-05-21-1752 arXiv:2407.17966 [quant-ph]

2025 arXiv
[13]

Liyi Li, Finn Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, and Michael Hicks. 2022. Verified Compilation of Quantum Oracles.Proc. ACM Program. Lang.6, OOPSLA2 (Oct. 2022), 146:589–146:615. doi:10.1145/3563309

2022 doi
[14]

Chia-Chun Lin and Niraj K. Jha. 2014. RMDDS: Reed-muller Decision Diagram Synthesis of Reversible Logic Circuits. J. Emerg. Technol. Comput. Syst.10, 2 (March 2014), 14:1–14:25. doi:10.1145/2564923

2014 doi
[15]

Maslov, G

D. Maslov, G. W. Dueck, and D. M. Miller. 2007. Techniques for the synthesis of reversible Toffoli networks.ACM Trans. Des. Autom. Electron. Syst.12, 4 (Sept. 2007), 42–es. doi:10.1145/1278349.1278355

2007
[16]

Michael Miller, Dmitri Maslov, and Gerhard W

D. Michael Miller, Dmitri Maslov, and Gerhard W. Dueck. 2003. A transformation based algorithm for reversible logic synthesis. InProceedings of the 40th Annual Design Automation Conference(Anaheim, CA, USA)(DAC ’03). Association for Computing Machinery, New York, NY, USA, 318–...

2003
[17]

2000.Quantum Programming in QCL

Bernhard Ömer. 2000.Quantum Programming in QCL. Diploma Thesis. Technische Universität Wien, Vienna, Austria. http://hdl.handle.net/20.500.12708/182261

2000
[18]

Anouk Paradis, Benjamin Bichsel, Samuel Steffen, and Martin Vechev. 2021. Unqomp: Synthesizing Uncomputation in Quantum Circuits. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM, Virtual Canada, 222–236. doi...

2021
[19]

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

2024 doi
[20]

Alex Parent, Martin Roetteler, and Krysta M. Svore. 2015. Reversible circuit compilation with space constraints. arXiv:1510.00377 [quant-ph] https://arxiv.org/abs/1510.00377

2015 arXiv
[21]

Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic. 2019. ReQWIRE: Reasoning about Reversible Quan- tum Circuits. InProceedings of the 15th International Conference on Quantum Physics and Logic (QPL 2018) (Electronic Proceedings in Theoretical Computer Science, Vol...

2019 arXiv
[22]

Robert Rand, Jennifer Paykin, and Steve Zdancewic. 2018. QWIRE Practice: Formal Verification of Quantum Circuits in Coq.Electronic Proceedings in Theoretical Computer Science266 (Feb. 2018), 119–132. doi:10.4204/EPTCS.266.8 arXiv:1803.00699 [cs]

2018 arXiv
[23]

Mehdi Saeedi and Igor L. Markov. 2013. Synthesis and Optimization of Reversible Circuits—a Survey.ACM Comput. Surv.45, 2 (March 2013), 21:1–21:34. doi:10.1145/2431211.2431220

2013
[24]

Raphael Seidel, Nikolay Tcholtchev, Sebastian Bock, and Manfred Hauswirth. 2023. Uncomputation in the Qrisp High-Level Quantum Programming Framework. InReversible Computation: 15th International Conference, RC 2023, Giessen, Germany, July 18–19, 2023, Proceedings(Giessen, Germ...

2023 doi
[25]

Alireza Shafaei, Mehdi Saeedi, and Massoud Pedram. 2013. Reversible Logic Synthesis of K-Input, m-Output Lookup Tables. InDesign, Automation & Test in Europe Conference & Exhibition (DATE), 2013. IEEE Conference Publications, Grenoble, France, 1235–1240. doi:10.7873/DATE.2013.256

2013 doi
[26]

Ritvik Sharma and Sara Achour. 2025. Optimizing Ancilla-Based Quantum Circuits with SPARE.Proc. ACM Program. Lang.9, PLDI (June 2025), 154:176–154:200. doi:10.1145/3729253

2025 doi
[27]

Peter W. Shor. 1997. Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer.SIAM J. Comput.26, 5 (1997), 1484–1509

1997
[28]

Bonan Su, Li Zhou, Yuan Feng, and Mingsheng Ying. 2026. Borrowing Dirty Qubits in Quantum Programs. InProceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2(USA)(ASPLOS ’26). Association for Compu...

2026
[29]

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

2018
[30]

Michael Kirkedal Thomsen. 2012. A Functional Language for Describing Reversible Logic. InProceeding of the 2012 Forum on Specification and Design Languages. IEEE, Vienna, Austria, 135–142

2012
[31]

Hristo Venev, Timon Gehr, Dimitar Dimitrov, and Martin Vechev. 2024. Modular Synthesis of Efficient Quantum Uncomputation.Proc. ACM Program. Lang.8, OOPSLA2 (Oct. 2024), 345:2097–345:2124. doi:10.1145/3689785 28 Wu and Deng

2024 doi
[32]

Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks. 2023. Qunity: A Unified Language for Quantum and Classical Computing.Proc. ACM Program. Lang.7, POPL (Jan. 2023), 32:921–32:951. doi:10.1145/3571225

2023 doi
[33]

2010.Towards a design flow for reversible logic

Robert Wille and Rolf Drechsler. 2010.Towards a design flow for reversible logic. Springer Netherlands. doi:10.1007/978- 90-481-9579-4

2010 doi
[34]

Robert Wille, Sebastian Offermann, and Rolf Drechsler. 2010. SyReC: A Programming Language for Synthesis of Reversible Circuits. In2010 Forum on Specification & Design Languages (FDL 2010). IET, Southampton, UK, 1–6. doi:10.1049/ic.2010.0150

2010
[35]

Mingsheng Ying and Zhicheng Zhang. 2024. Verification of Recursively Defined Quantum Circuits. doi:10.48550/ arXiv.2404.05934 arXiv:2404.05934 [quant-ph]

2024 doi arXiv
[36]

Charles Yuan and Michael Carbin. 2022. Tower: Data Structures in Quantum Superposition.Proceedings of the ACM on Programming Languages6, OOPSLA2 (Oct. 2022), 259–288. doi:10.1145/3563297

2022 doi
[37]

Charles Yuan, Agnes Villanyi, and Michael Carbin. 2024. Quantum Control Machine: The Limits of Control Flow in Quantum Programming.Proceedings of the ACM on Programming Languages8, OOPSLA1 (April 2024), 1–28. doi:10.1145/3649811

2024 doi
[38]

per-level immediate cleanup

Zhicheng Zhang and Mingsheng Ying. 2025. Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs.Proceedings of the ACM on Programming Languages9, PLDI (June 2025), 822–847. doi:10.1145/ 3729283 arXiv:2408.10054 [quant-ph] A Comparing RQIMP to RQC ++ F...

2025 arXiv
[2020]

In2020 ACM/IEEE 47th Annual International Symposium on Computer Architecture (ISCA)

SQUARE: Strategic Quantum Ancilla Reuse for Modular Quantum Programs via Cost-Effective Uncomputation. In2020 ACM/IEEE 47th Annual International Symposium on Computer Architecture (ISCA). IEEE, Valencia, Spain, 570–583. doi:10.1109/ISCA45697.2020.00054

Pith tools

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

[1] [1]

Abhari, Arvin I

Ali J. Abhari, Arvin I. Faruque, Mohammad Javad Dousti, Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, and Fred Chong. 2012.Scaffold: Quantum Programming Language. Technical Report. Princeton University. https://api.semanticscholar.org/CorpusID:18354908

work page 2012

[2] [2]

Andris Ambainis, Kaspars Balodis, J ¯anis Iraids, Martins Kokainis, Krišj ¯anis Pr ¯usis, and Jevg ¯enijs Vihrovs. 2018. Quantum Speedups for Exponential-Time Dynamic Programming Algorithms. doi:10.48550/arXiv.1807.05209 arXiv:1807.05209 [quant-ph]

work page Pith review arXiv doi:10.48550/arxiv.1807.05209 2018

[3] [3]

Matthew Amy, Martin Roetteler, and Krysta M. Svore. 2017. Verified Compilation of Space-Efficient Reversible Circuits. InComputer Aided Verification - 29th International Conference, CA V 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II (Lecture Notes in Computer Science), Rupak Majumdar and Viktor Kuncak (Eds.). Springer, 3–21. doi:10.100...

work page doi:10.1007/978-3-319-63390-9_1 2017

[4] [4]

C. H. Bennett. 1973. Logical reversibility of computation.IBM J. Res. Dev.17, 6 (Nov. 1973), 525–532. doi:10.1147/rd. 176.0525

doi:10.1147/rd 1973

[5] [5]

Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. 2020. Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics. InProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, London UK, 286–300. doi:10.1145/3385412.3386007

arXiv 2020

[6] [6]

Yongshan Ding, Xin-Chuan Wu, Adam Holmes, Ash Wiseth, Diana Franklin, Margaret Martonosi, and Frederic T. Chong

[7] [7]

Christoph Durr, Mark Heiligman, Peter Hoyer, and Mehdi Mhalla. 2006. Quantum Query Complexity of Some Graph Problems.SIAM J. Comput.35, 6 (Jan. 2006), 1310–1328. doi:10.1137/050644719 arXiv:quant-ph/0401091

work page Pith review arXiv 2006

[8] [8]

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 programming language. InProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation(Seattle, Washington, USA)(PLDI ’13). Association for Computing Machinery, New York, NY, USA, 333–342. doi:10...

arXiv 2013