Pith. sign in

REVIEW 4 major objections 5 minor 78 references

The paper claims that quantum programs can be specified as compositions of register-level operations—without naming individual gates—and demonstrates the claim with a quantum SMT solver.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

A formal framework for structured quantum programming where operations act on entire quantum registers, demonstrated by a quantum SMT solver prototype.

T0 review reviewed 2026-08-05 challenge →

load-bearing objection Register-level structured programming is a sensible next step for quantum software engineering, but the formalization has load-bearing gaps that the SMT application paper does not fully cover. the 4 major comments →

arxiv 2608.03873 v1 pith:CEB6P7KK submitted 2026-08-04 quant-ph cs.SE

High-level quantum structured programs as quantum registers compositions

David Chamizo , Jose Garcia-Alonso , Juan M. Murillo This is my paper
classification quant-ph cs.SE
keywords quantum programmingquantum registersstructured programmingabstractionquantum SMT solverphase operationsamplitude amplificationquantum software engineering
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The reading

This paper argues that quantum programs should be written as compositions of whole-register transformations rather than sequences of gates on individual qubits. The authors formalize four such transformations—PhaseAND, PhaseOR, Reflection, and Synchronization—using an algebraic semantics that connects high-level syntax to low-level circuits. To show these operations are sufficient, they design a quantum satisfiability-modulo-theories (SMT) solver using only those operations plus data-encoding oracles, and they validate it by simulation on two small formulas. If the proposal holds, it would give quantum programmers a structured, modular style closer to classical high-level programming and less prone to gate-level specification errors.

Core claim

The central claim is that a quantum computation can be treated as an evolving structure of registers, and that a meaningful end-to-end program can be specified at that level alone. The paper defines a register as valid for logical evaluation when its state factors into a value subspace and ancilla qubits that evaluate logical predicates for every value in superposition. It then shows that PhaseAND, PhaseOR, Reflection, and Synchronization have algebraic definitions and circuit realizations, and it proves within the formalism that a multi-controlled phase on an auxiliary qubit is equivalent to a controlled phase on an ancilla. Using these operations, the SMT solver marks satisfying assignment

What carries the argument

The machinery is the register-with-ancilla form of Eq. (12): each register's Hilbert space splits into a value subspace and ancilla qubits that evaluate logical predicates for every value in superposition. All four transformations are defined on this structure—PhaseAND and PhaseOR as multi-controlled phase operations gated on ancillas, Reflection as a basis change plus PhaseNAND, and Synchronization as fan-out of one register's value across others in a GHZ-like entangled way. The algebraic laws of quantum conditionals carry the low-level semantics, allowing equivalences and optimizations to be proven before gate decomposition.

Load-bearing premise

Every predicate the program needs to evaluate must be encodable as extra qubits attached to a register, with the predicate outcome computed coherently for every value in superposition and then cleanly erased; if any predicate resists that encoding, the register-level operations no longer behave as specified.

What would settle it

Run the same solver structure on a satisfiable formula whose atoms use a theory not covered by the paper's oracle examples, such as nonlinear integer arithmetic (e.g., x·y = z); if the measured outcomes deviate from the predicted amplitude-amplification iteration count, or the ancillas are not restored to |0...0>, the assumed universality of the register encoding is falsified.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • A quantum programming language could expose PhaseAND, PhaseOR, Reflection, and Synchronization as built-in primitives, letting programmers specify algorithms at register level while the language handles gate translation, uncomputation, and auxiliary qubits.
  • Because the transformations carry algebraic semantics, program sequences can be simplified and verified before circuit synthesis; the paper demonstrates one equivalence proof and one sequence optimization of this kind.
  • The SMT solver's structure is theory-agnostic: only the oracle encoding depends on the data type, so the same program skeleton applies to any theory with a suitable oracle, not just the modular integer arithmetic tested.
  • Reflection subsumes a family of amplitude-amplification and fixed-point search schemes, so algorithms built from repeated reflections can be written in the same high-level style.
  • Register-level operations have analyzed implementation costs (multi-controlled gates can be linear-depth; synchronization can be logarithmic-depth with fan-out), giving programmers a complexity model independent of the low-level gate set.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • A testable extension is to push the SMT solver toward theories without off-the-shelf oracle generators, such as nonlinear arithmetic, and check whether the register-plus-ancilla encoding remains constructible and cleanly uncomputable; the paper does not demonstrate this.
  • The paper's hand-derived algebraic optimization suggests that a compiler could restructure entire programs before gate synthesis, but the advantage over gate-level optimizers is not measured; that comparison is an open question.
  • Synchronization behaves like a no-cloning-safe broadcast, so the same pattern could generalize to data-parallel quantum algorithms where one value fans out across many registers, is processed in parallel, and is reduced by phase operations.
  • Validation is limited to small formulas under simulation; moving to many clauses and constructs would make the width-versus-depth trade-off between synchronization and concatenated evaluation measurable.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 5 minor

Summary. This paper proposes a register-level abstraction for quantum programming. The central objects are quantum registers viewed as computational constructs with a value subspace and ancilla qubits encoding predicates. The authors formalize four transformations -- PhaseAND(theta), PhaseOR(theta), Reflection, and Synchronization -- using the algebraic quantum-circuit formalism of Ying et al. [25], and they use these transformations to express Grover-style amplitude amplification for a quantum SMT solver (Algorithm 1). Validation is carried out in Qiskit on two formulas, one single-construct and one multi-construct, with solutions reported in Figs. 3 and 5. The paper's main claim is that this demonstrates a high-level, gate-independent structured programming methodology.

Significance. The ambition is important: if the formalizations were complete, the paper would provide a genuine step toward structured quantum programming at the register level, with algebraic laws available for optimization and verification. The concrete strengths are the use of an existing algebraic semantics, a worked equivalence proof in Section IV-G, and an SMT example with a deposited reproducibility repository. However, the formalization as written has two load-bearing gaps -- the quantum-if syntax is used outside its defined domain, and the Reflection rule is not justified for the entangling initializations used by Algorithm 1. These are fixable but currently prevent the central claim from being accepted as it stands.

major comments (4)
  1. [Section IV-E, Eq. (21) and Section V-C, Algorithm 1] Eq. (21) formalizes REFLPi_ki by conjugation with seq_i C_{ki}, i.e. a tensor product of per-register initialization unitaries. The simplification to qif (wedge_i Pi_{ki,qi}) then skip else Ph_pi is valid only for such product unitaries. Algorithm 1 initializes each construct's registers with SYNC_unif[q_{S_i}] (lines 2 and 19); for |S_i|>1 this creates an entangled GHZ-like state. The full initialization C is then entangling, so C^dagger(REFLPi0)C is not the conditional product-reflector of Eq. (21). The solver's reflection step is therefore not an instance of the formalized REFL operation as written. Either extend Eq. (21) to entangling initializations with a proof, or revise Algorithm 1 so the reflection uses the formalized product initialization.
  2. [Section IV-C, Eq. (14)] The qif syntax defined in Eq. (1) requires the branch states to form an orthonormal basis of the control register's Hilbert space. Eq. (14) uses branch states |psi_{x_i}>|1>^{otimes n_i} over all data values, omitting all ancilla configurations with at least one |0>; this set is not a basis. Since PhaseAND is the foundation for PhaseNAND, PhaseOR, and Reflection, all subsequent formalizations inherit this gap unless a semantics for 'qif over a non-complete orthonormal subset' is defined and justified.
  3. [Section IV-C, Eq. (15)] The derivation of PhaseNAND relies on 'applying circuit Ph_{-theta} to any qubit of the entangled state.' If Ph_theta means the global phase e^{i theta} I on the whole system, the statement should be stated explicitly; if it means the single-qubit gate P_theta = diag(1,e^{i theta}), the claim is false for an entangled state because applying P_theta to one subsystem changes relative phases unless that subsystem is a tensor factor. The same notation is used again in Eq. (17) for PhaseOR, so this ambiguity is load-bearing and should be resolved.
  4. [Section V-B, Eq. (35) and Section IV-B, Eq. (12)] The SMT construction assumes that every theory predicate can be coherently evaluated in ancillas and then cleanly uncomputed. The paper cites [74] for modular arithmetic comparators but gives no condition on the theory signature or oracle complexity for arbitrary SMT theories. The abstract's general claim should be restricted to theories for which such oracle encodings exist, or the oracle assumption should be made an explicit formal part of the framework.
minor comments (5)
  1. [Section II] Typo: 'lacks a a proper model' should read 'lacks a proper model'.
  2. [Section V-C, Algorithm 1, line 19] The parenthetical '(seq_{j in S_i} C_{k_j} equiv SYNC_unif[q_{S_i}], forall i)' is unclear: it seems to identify a tensor product of per-register initializations with an entangling synchronization. This is precisely the point that needs either a proof or a reformulation, and the current wording should be rewritten.
  3. [Section IV-G] The optimization example in Eq. (26)-(27) would benefit from explicitly stating the domain of the variables q_i and the target ancilla; as written, the conditional notation mixes a multi-register control with a single target ancilla without defining the convention.
  4. [Section IV-H] Minor wording: 'all-to-allconnectivity' lacks a space, and 'size do not pose a problem' should be 'sizes do not pose a problem'.
  5. [Section V-D] The remark that transformations are 'generalized ad hoc' for Qiskit is honest but should be reconciled with the claim that the program is designed solely from the formalized operations; otherwise the simulation validates the informal intent rather than the formal semantics.

Circularity Check

0 steps flagged

No significant circularity: the formalized operations are definitions, the SMT solver is a constructive application with independent oracle support, and the validation is a real simulation.

full rationale

The paper does not derive a prediction from its own inputs. The formalized operations PhaseAND, PhaseOR, REFL, and SYNC are defined directly using the external algebraic formalism of Ying et al. [25], and their definitions do not rely on the SMT solver or on the paper's conclusions. The quantum SMT solver is assembled from these operations following the independent Grover/Lin et al. scheme, and its correctness is demonstrated by simulation, not by construction from the formalism. The self-citation to the authors' own oracle-construction paper [74] provides an externally published implementation of the less-than comparator and is not load-bearing for the conceptual framework. The formalization gap noted by the skeptic (Eq. (21) applies to tensor-product initializations, whereas Algorithm 1 uses SYNC_unif) is a soundness/correctness concern, not a circularity: the solver's output is not equivalent to its inputs by construction. Accordingly, no circular step can be quoted and exhibited, and the paper receives a score of 0.

Axiom & Free-Parameter Ledger

1 free parameters · 5 axioms · 1 invented entities

The framework rests on the imported algebraic laws of quantum circuits, on the ancilla-based register structure, and on a few questionable implementation assumptions (global phase via a single qubit, extended if-statement syntax). No data fitting is used for the core transformations; the only fitted-style choice is the Grover iteration count in the validation.

free parameters (1)
  • k, number of Grover iterations = exact count based on known solution set for the test formulas
    In Algorithm 1, 'Calculate number of iterations k' is unspecified; the validation uses the exact ideal count for the chosen formulas, which requires knowing the number of solutions. This is a free choice that affects the displayed results.
axioms (5)
  • domain assumption Algebraic laws of quantum circuits from Ying et al. [25] are valid and applicable to the register-level transformations.
    Section III imports laws (3)-(10) without proof and Section IV relies on them for the syntax/semantics mapping.
  • domain assumption Every register can be decomposed as H_val ⊗ H_anc where ancillas evaluate arbitrary predicates without changing the value subspace.
    Section IV-B, Eq. (12) postulates this factorization; all transformations PhaseAND, PhaseOR, Reflection depend on it.
  • ad hoc to paper A global phase shift can be implemented by applying a phase gate to any single qubit of the entangled state.
    Section IV-C, Eq. (15) uses this; it is not generally true for an entangled qubit unless the phase is truly global, and the paper does not consistently describe an auxiliary-qubit construction.
  • ad hoc to paper The quantum-if notation can be used over non-complete orthonormal subsets, for example states with all ancillas equal to |1>.
    Eq. (14) uses branching over data states with ancillas all 1, a subset of the basis, which is not defined in the original formalism Eq. (1).
  • domain assumption Oracles for arbitrary SMT predicates can be implemented coherently with the ancilla structure.
    Section V-B defines oracles abstractly; actual comparator implementations are cited from [74], but no proof is given that they fit the exact structure of Eq. (12) for all theories.
invented entities (1)
  • Computational construct no independent evidence
    purpose: A high-level abstraction where a quantum register models an entity, such as water levels or integer variables, whose possible states are basis elements.
    Conceptual modeling device introduced in Section IV-A; not a physical postulate, but central to the framework's language.

reviewed 2026-08-05 · how reviews work

0 comments
Cite this review

Pith. "Pith review of High-level quantum structured programs as quantum registers compositions." pith.science (2026). https://pith.science/paper/CEB6P7KK

@misc{pith2026260803873,
  author       = {Pith},
  title        = {Pith review of: High-level quantum structured programs as quantum registers compositions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CEB6P7KK}},
  note         = {Machine review of arXiv:2608.03873}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Current quantum programs are mainly designed at the level of quantum gates acting on individual qubits; on a large scale and for complex problems this may involve a high cognitive load on the programmer, making the program specification nontrivial and error-prone. In this context, providing quantum programming with higher abstraction mechanisms will assist in making this task more manageable and robust against design errors. In this work, a conceptual framework is addressed following the notion of the whole quantum computation as a structure composed of quantum registers representing each an undivided entity. Thus, computation progresses through semantically well-defined transformations that act on, or entangle, quantum registers, thereby modifying the global state. Ultimately, the program reaches the desired state by following a specific composition strategy. With this in mind, high-level syntax is presented through an algebraic formalism that bridges them with their low-level semantics. Proposed syntax is based on certain well-know operations used on quantum algorithms that apply phase shifts upon logical condition satisfaction or leverage on parallel evaluation. Based solely on the formalized operations, a quantum satisfiability modulo theories (SMT) solver can be designed. At its core, this work contributes to establishing some methodological principles towards realizing a high-level quantum structured programming.

Figures

Figures reproduced from arXiv: 2608.03873 by David Chamizo, Jose Garcia-Alonso, Juan M. Murillo.

Figure 1
Figure 1. Figure 1: Representation of the P haseAND(θ) operation functionality on two register with one constraint each. On the right, those states without amplitude contribution are suppressed for simplification. Bars height is an arbitrary depiction of amplitude absolute values while color is related to relative phase. qubit q. In particular, circuit P hθ generates a global θ-phase shift. Inherently, this phase shift is exc… view at source ↗
Figure 2
Figure 2. Figure 2: Representation of the P haseOR(θ) operation functionality on two register with one constraint each. On the right, those states without amplitude contribution are suppressed for simplification. Bars height is an arbitrary depiction of amplitude absolute values while color is related to relative phase. Hence, the abstraction P haseNOR(θ) (or P h¬(∨),θ) can be constructed from P h∧ in a sequence along the inp… view at source ↗
Figure 3
Figure 3. Figure 3: Histogram representing the results obtained after evaluating Algorithm 1 [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Circuit derived from the high-level syntax of Algorithm 1 for the case [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Histogram representing the results obtained after evaluating Algorithm 1 [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

78 extracted references · 58 canonical work pages · 1 internal anchor

  1. [1]

    Simulating physics with computers,

    R. P. Feynman, “Simulating physics with computers,”International Journal of Theoretical Physics, vol. 21, no. 6–7, pp. 467–488, 1982

    1982

  2. [2]

    Quantum theory, the Church–Turing principle and the universal quantum computer,

    D. Deutsch, “Quantum theory, the Church–Turing principle and the universal quantum computer,”Proceedings of the Royal Society of London. A., vol. 400, no. 1818, pp. 97–117, 1985

    work page 1985

  3. [3]

    A fast quantum mechanical algorithm for database search,

    L. K. Grover, “A fast quantum mechanical algorithm for database search,” inProceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, p. 212–219, 1996

    work page 1996

  4. [4]

    Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer,

    P. W. Shor, “Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer,”SIAM Journal on Computing, vol. 26, no. 5, pp. 1484–1509, 1997

    1997

  5. [5]

    Quantum supremacy using a programmable supercon- ducting processor,

    F. Aruteet al., “Quantum supremacy using a programmable supercon- ducting processor,”Nature, vol. 574, no. 7779, pp. 505–510, 2019

    work page 2019

  6. [6]

    Materials challenges and opportunities for quantum computing hardware,

    N. P. De Leonet al., “Materials challenges and opportunities for quantum computing hardware,”Science, vol. 372, no. 6539, 2021

    work page 2021

  7. [7]

    Quantum hardware devices (qhds): Opportunities and challenges,

    A. Oukaira, “Quantum hardware devices (qhds): Opportunities and challenges,”IEEE Access, vol. 13, pp. 98229–98241, 2025

    work page 2025

  8. [8]

    Quantum algorithms: A survey of applications and end-to-end complexities,

    A. M. Dalzellet al., “Quantum algorithms: A survey of applications and end-to-end complexities,”arXiv preprint arXiv:2310.03011, 2023

    Pith/arXiv arXiv 2023

  9. [9]

    Quantum error correction,

    T. A. Brun, “Quantum error correction,”Oxford Research Encyclopedia of Physics, 2020

    work page 2020

  10. [10]

    Quantum software engineering: Roadmap and challenges ahead,

    J. M. Murilloet al., “Quantum software engineering: Roadmap and challenges ahead,”ACM Transactions on Software Engineering and Methodology, vol. 34, no. 5, 2025

    work page 2025

  11. [11]

    IBM quantum computers: evolution, performance, and future directions,

    M. AbuGhanem, “IBM quantum computers: evolution, performance, and future directions,”arXiv preprint arXiv:2410.00916, 2024

    Pith/arXiv arXiv 2024

  12. [12]

    Correction to: Advancements in superconducting quantum computing,

    Y .-Y . Jianget al., “Correction to: Advancements in superconducting quantum computing,”National Science Review, vol. 13, no. 2, p. nwaf582, 2026

    work page 2026

  13. [13]

    Quantum software engineering: Landscapes and horizons,

    J. Zhao, “Quantum software engineering: Landscapes and horizons,” arXiv preprint arXiv:2007.07047, 2020

    Pith/arXiv arXiv 2007

  14. [14]

    Quantum programming languages,

    B. Heimet al., “Quantum programming languages,”Nature Reviews Physics, vol. 2, pp. 709–722, 2020

    work page 2020

  15. [15]

    Scaffold: Quantum programming language,

    A. J. Abhariet al., “Scaffold: Quantum programming language,” tech. rep., Princeton University, 2012

    work page 2012

  16. [16]

    Quipper: a scalable quantum programming language,

    A. S. Green, P. L. Lumsdaine, N. J. Ross, P. Selinger, and B. Valiron, “Quipper: a scalable quantum programming language,”ACM SIGPLAN Notices, vol. 48, no. 6, p. 333–342, 2013

    work page 2013

  17. [17]

    Q# enabling scalable quantum computing and develop- ment with a high-level dsl,

    K. Svoreet al., “Q# enabling scalable quantum computing and develop- ment with a high-level dsl,” inProceedings of the Real World Domain Specific Languages Workshop 2018, no. 7, pp. 1–10, 2018

    work page 2018

  18. [18]

    PennyLane: Automatic differentiation of hybrid quantum-classical computations,

    V . Bergholmet al., “PennyLane: Automatic differentiation of hybrid quantum-classical computations,”arXiv preprint arXiv:1811.04968, 2022

    Pith/arXiv arXiv 2022

  19. [19]

    Quantum computing with Qiskit,

    A. Javadi-Abhariet al., “Quantum computing with Qiskit,”arXiv preprint arXiv:2405.08810, 2024

    Pith/arXiv arXiv 2024

  20. [20]

    Cirq Developers, “Cirq,”Zenodo, 2025

    work page 2025

  21. [21]

    M. V . Wilkes, D. J. Wheeler, and S. Gill,The preparation of programs for an electronic digital computer. Addison-Wesley Press, 2nd ed., 1957

    work page 1957

  22. [22]

    The art of abstraction in quantum software,

    O. Di Matteo, “The art of abstraction in quantum software,” in2025 IEEE/ACM International Workshop on Quantum Software Engineering (Q-SE), pp. 25–26, IEEE, 2025

    work page 2025

  23. [23]

    Ying,Foundations of quantum programming

    M. Ying,Foundations of quantum programming. Morgan Kaufmann by Elsevier, 2nd ed., 2024

    work page 2024

  24. [24]

    On the need of quantum-oriented paradigm,

    S. Ali and T. Yue, “On the need of quantum-oriented paradigm,” in Proceedings of the 2nd International Workshop on Quantum Programming for Software Engineering, pp. 17–20, 2023

    work page 2023

  25. [25]

    Laws of quantum programming,

    M. Ying, L. Zhou, and G. Barthe, “Laws of quantum programming,” ACM Transactions on Software Engineering and Methodology, vol. 35, no. 7, 2026

    work page 2026

  26. [26]

    Programming with abstract data types,

    B. Liskov and S. Zilles, “Programming with abstract data types,”ACM SIGPLAN Notices, vol. 9, no. 4, pp. 50–59, 1974

    work page 1974

  27. [27]

    Model checking and abstraction,

    E. M. Clarke, O. Grumberg, and D. E. Long, “Model checking and abstraction,”ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 16, no. 5, pp. 1512–1542, 1994

    work page 1994

  28. [28]

    C. Y . Baldwin and K. B. Clark,Design rules, volume 1: The power of modularity. MIT Press, 2000

    work page 2000

  29. [29]

    Quantum computational networks,

    D. E. Deutsch, “Quantum computational networks,”Proceedings of the Royal Society of London. A., vol. 425, no. 1868, pp. 73–90, 1989

    work page 1989

  30. [30]

    Quantum circuit complexity,

    A. Chi-Chih Yao, “Quantum circuit complexity,” inProceedings of 1993 IEEE 34th Annual Foundations of Computer Science, pp. 352–361, 1993

    work page 1993

  31. [31]

    QuECT: A New Quantum Programming Paradigm

    A. Chakraborty, “QuECT: A new quantum programming paradigm,” arXiv preprint arXiv:1104.0497, 2011

    work page internal anchor Pith review Pith/arXiv arXiv 2011

  32. [32]

    A quantum engineer’s guide to superconducting qubits,

    P. Krantz, M. Kjaergaard, F. Yan, T. P. Orlando, S. Gustavsson, and W. D. Oliver, “A quantum engineer’s guide to superconducting qubits,” Applied Physics Reviews, vol. 6, no. 2, p. 021318, 2019

    2019

  33. [33]

    Silq: A high-level quantum language with safe uncomputation and intuitive semantics,

    B. Bichsel, M. Baader, T. Gehr, and M. Vechev, “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, pp. 286–300, 2020

    work page 2020

  34. [34]

    Qrisp: A framework for compilable high-level programming of gate-based quantum computers,

    R. Seidelet al., “Qrisp: A framework for compilable high-level programming of gate-based quantum computers,”arXiv preprint arXiv:2406.14792, 2024

    Pith/arXiv arXiv 2024

  35. [35]

    Designing a meta-model for the eclipse qrisp edsl for high-level quantum programming,

    S. Bock, R. Seidel, M. Petriˇc, N. Tcholtchev, A. Hoffmann, and N. Porges, “Designing a meta-model for the eclipse qrisp edsl for high-level quantum programming,” inProceedings of the 13th International Conference on Model-Based Software and Systems Engineering - MODELSWARD, vol. 1, pp. 27–39, SciTePress, 2025

    work page 2025

  36. [36]

    Qmod: Expressive high-level quantum modeling,

    M. Vaxet al., “Qmod: Expressive high-level quantum modeling,”arXiv preprint arXiv:2502.19368, 2025

    Pith/arXiv arXiv 2025

  37. [37]

    Quantum algorithms revisited,

    R. Cleve, A. Ekert, C. Macchiavello, and M. Mosca, “Quantum algorithms revisited,”Proceedings of the Royal Society of London. A., vol. 454, no. 1969, pp. 339–354, 1998

    work page 1969

  38. [38]

    Revisiting abstractions for software architecture and tools to support them,

    M. Shaw, D. V . Klein, and T. L. Ross, “Revisiting abstractions for software architecture and tools to support them,”IEEE Transactions on Software Engineering, vol. 51, no. 3, pp. 768–773, 2025

    work page 2025

  39. [39]

    An abstraction hierarchy toward productive quantum programming,

    O. Di Matteo, S. N ´u˜nez-Corrales, M. Stechły, S. P. Reinhardt, and T. Mattson, “An abstraction hierarchy toward productive quantum programming,” in2024 IEEE International Conference on Quantum Computing and Engineering (QCE), pp. 979–989, IEEE, 2024

    work page 2024

  40. [40]

    Increasing the level of abstraction as a strategy for accelerating the adoption of complex technologies,

    W. C. Shih, “Increasing the level of abstraction as a strategy for accelerating the adoption of complex technologies,”Strategy Science, vol. 6, no. 1, pp. 54–61, 2021

    work page 2021

  41. [41]

    Object-oriented programming: Some history, and challenges for the next fifty years,

    A. P. Black, “Object-oriented programming: Some history, and challenges for the next fifty years,”Information and Computation, vol. 231, pp. 3–20, 2013

    work page 2013

  42. [42]

    Quantum networks for elementary arithmetic operations,

    V . Vedral, A. Barenco, and A. Ekert, “Quantum networks for elementary arithmetic operations,”Physical Review A, vol. 54, no. 1, p. 147, 1996

    work page 1996

  43. [43]

    Addition on a quantum computer,

    T. G. Draper, “Addition on a quantum computer,”arXiv preprint quant- ph/0008033, 2000

    arXiv 2000

  44. [44]

    Quantum circuit synthesis and compilation optimization: Overview and prospects,

    G. Yanet al., “Quantum circuit synthesis and compilation optimization: Overview and prospects,”arXiv preprint arXiv:2407.00736, 2025

    arXiv 2025

  45. [45]

    Design and synthesis of scalable quantum programs,

    T. Goldfriendet al., “Design and synthesis of scalable quantum programs,” arXiv preprint arXiv:2412.07372, 2025

    Pith/arXiv arXiv 2025

  46. [46]

    When abstraction breaks physics: Rethinking modular design in quantum software,

    J. Zhao, “When abstraction breaks physics: Rethinking modular design in quantum software,” in2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 3886–3890, 2025

    work page 2025

  47. [47]

    Laws of programming,

    C. Hoareet al., “Laws of programming,”Communications of the ACM, vol. 30, no. 8, pp. 672–686, 1987

    work page 1987

  48. [48]

    Verification of recursively defined quantum circuits,

    M. Ying and Z. Zhang, “Verification of recursively defined quantum circuits,”arXiv preprint arXiv:2404.05934, 2024

    Pith/arXiv arXiv 2024

  49. [49]

    Quantum amplitude amplification and estimation,

    G. Brassard, P. Hoyer, M. Mosca, and A. Tapp, “Quantum amplitude amplification and estimation,”arXiv preprint quant-ph/0005055, 2000

    Pith/arXiv arXiv 2000

  50. [50]

    Quantum speed-up of markov chain based algorithms,

    M. Szegedy, “Quantum speed-up of markov chain based algorithms,” in45th Annual IEEE Symposium on Foundations of Computer Science, pp. 32–41, 2004

    work page 2004

  51. [51]

    Going beyond Bell’s theorem,

    D. M. Greenberger, M. A. Horne, and A. Zeilinger, “Going beyond Bell’s theorem,” inKafatos, M. (eds) Bell’s Theorem, Quantum Theory and Conceptions of the Universe. Fundamental Theories of Physics, vol. 37, pp. 69–72, Springer, 1989

    work page 1989

  52. [52]

    Parallel quantum computation and quantum codes,

    C. Moore and M. Nilsson, “Parallel quantum computation and quantum codes,”SIAM Journal on Computing, vol. 31, no. 3, pp. 799–815, 2001

    work page 2001

  53. [53]

    Logical reversibility of computation,

    C. H. Bennett, “Logical reversibility of computation,”IBM Journal of Research and Development, vol. 17, no. 6, pp. 525–532, 1973

    1973

  54. [54]

    Fixed-point quantum search,

    L. K. Grover, “Fixed-point quantum search,”Physical Review Letters, vol. 95, no. 15, p. 150501, 2005

    work page 2005

  55. [55]

    Fixed-point quantum search with an optimal number of queries,

    T. J. Yoder, G. H. Low, and I. L. Chuang, “Fixed-point quantum search with an optimal number of queries,”Physical Review Letters, vol. 113, no. 21, p. 210501, 2014

    work page 2014

  56. [56]

    Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics,

    A. Gily ´en, Y . Su, G. H. Low, and N. Wiebe, “Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics,” inProceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, pp. 193–204, 2019

    work page 2019

  57. [57]

    Grand unification of quantum algorithms,

    J. M. Martyn, Z. M. Rossi, A. K. Tan, and I. L. Chuang, “Grand unification of quantum algorithms,”PRX Quantum, vol. 2, no. 4, p. 040203, 2021

    2021

  58. [58]

    Hamiltonian simulation by qubitization,

    G. H. Low and I. L. Chuang, “Hamiltonian simulation by qubitization,” Quantum, vol. 3, p. 163, 2019

    work page 2019

  59. [59]

    Quantum support vector machine for big data classification,

    P. Rebentrost, M. Mohseni, and S. Lloyd, “Quantum support vector machine for big data classification,”Physical Review Letters, vol. 113, p. 130503, 2014

    work page 2014

  60. [60]

    Quantum machine learning,

    J. Biamonte, P. Wittek, N. Pancotti, P. Rebentrost, N. Wiebe, and S. Lloyd, “Quantum machine learning,”Nature, vol. 549, pp. 195–202, 2017

    2017

  61. [61]

    Quantum linear systems algorithms: a primer,

    D. Dervovic, M. Herbster, P. Mountney, S. Severini, N. Usher, and L. Wossnig, “Quantum linear systems algorithms: a primer,”arXiv preprint arXiv:1802.08227, 2018

    Pith/arXiv arXiv 2018

  62. [62]

    A single quantum cannot be cloned,

    W. K. Wootters and W. H. Zurek, “A single quantum cannot be cloned,” Nature, vol. 299, pp. 802–803, 1982

    work page 1982

  63. [63]

    Efficient Z gates for quantum computing,

    D. C. McKay, C. J. Wood, S. Sheldon, J. M. Chow, and J. M. Gambetta, “Efficient Z gates for quantum computing,”Physical Review A, vol. 96, p. 022330, 2017

    work page 2017

  64. [64]

    Elementary gates for quantum computation,

    A. Barencoet al., “Elementary gates for quantum computation,”Physical Review A, vol. 52, p. 3457, 1995

    work page 1995

  65. [65]

    Linear-depth quantum circuits for multiqubit controlled gates,

    A. J. Da Silva and D. K. Park, “Linear-depth quantum circuits for multiqubit controlled gates,”Physical Review A, vol. 106, p. 042602, 2022

    work page 2022

  66. [66]

    Efficient constructions for simulating multi controlled quantum gates,

    S. Balauca and A. Arusoaie, “Efficient constructions for simulating multi controlled quantum gates,” inInternational Conference on Computational Science, pp. 179–194, Springer, 2022

    work page 2022

  67. [67]

    Quantum circuit for multi-qubit Toffoli gate with optimal resource,

    J. Nie, W. Zi, and X. Sun, “Quantum circuit for multi-qubit Toffoli gate with optimal resource,”arXiv preprint arXiv:2402.05053, 2024

    Pith/arXiv arXiv 2024

  68. [68]

    Optimizing gate decomposition for high-level quantum programming,

    E. C. Rosa, E. I. Duzzioni, and R. De Santiago, “Optimizing gate decomposition for high-level quantum programming,”Quantum, vol. 9, p. 1659, 2025

    work page 2025

  69. [69]

    A parallel and distributed quantum sat solver based on entanglement and teleportation,

    S.-W. Lin, T.-F. Wang, Y .-R. Chen, Z. Hou, D. San´an, and Y . S. Teo, “A parallel and distributed quantum sat solver based on entanglement and teleportation,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 363–382, Springer, 2024

    work page 2024

  70. [70]

    A. R. Bradley and Z. Manna,The calculus of computation: decision procedures with applications to verification. Springer, 2007

    work page 2007

  71. [71]

    Satisfiability modulo theories: introduction and applications,

    L. De Moura and N. Bjørner, “Satisfiability modulo theories: introduction and applications,”Communications of the ACM, vol. 54, no. 9, pp. 69–77, 2011

    work page 2011

  72. [72]

    Satisfiability modulo theories,

    C. Barrett and C. Tinelli, “Satisfiability modulo theories,” inHandbook of Model Checking, pp. 305–343, Springer, 2018

    work page 2018

  73. [73]

    High-level quantum structured programs as quantum registers compositions,

    D. Chamizo, J. Garcia-Alonso, and J. M. Murillo, “High-level quantum structured programs as quantum registers compositions,”Zenodo, 2026. https://doi.org/10.5281/zenodo.19762069 (Accessed July 2026)

    work page doi:10.5281/zenodo.19762069 2026

  74. [74]

    Automatic generation of efficient oracles: The less-than case,

    J. Sanchez-Rivero, D. Talav ´an, J. Garcia-Alonso, A. Ruiz-Cort ´es, and J. M. Murillo, “Automatic generation of efficient oracles: The less-than case,”Journal of Systems and Software, vol. 219, p. 112203, 2025

    work page 2025

  75. [75]

    Quantum register machine: Efficient imple- mentation of quantum recursive programs,

    Z. Zhang and M. Ying, “Quantum register machine: Efficient imple- mentation of quantum recursive programs,”Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, pp. 822–847, 2025

    work page 2025

  76. [76]

    Quartz: superoptimization of quantum circuits,

    M. Xuet al., “Quartz: superoptimization of quantum circuits,” in Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 625–640, 2022

    work page 2022

  77. [77]

    Synthesizing quantum-circuit optimizers,

    A. Xu, A. Molavi, L. Pick, S. Tannu, and A. Albarghouthi, “Synthesizing quantum-circuit optimizers,”Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, pp. 835–859, 2023

    work page 2023

  78. [78]

    Twist: Sound reasoning for purity and entanglement in quantum programs,

    C. Yuan, C. McNally, and M. Carbin, “Twist: Sound reasoning for purity and entanglement in quantum programs,”Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, pp. 1–32, 2022

    work page 2022

This paper was first reviewed by deepseek-v4-flash on August 5, 2026.