Pith. sign in

REVIEW 2 major objections 5 minor 70 references

Integer hybrid path-sums give the first semi-automated static analysis that verifies hybrid quantum programs with unbounded loops and estimates their resource use.

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 ↗

T0 review · grok-4.5

2026-07-10 05:33 UTC pith:USOOGZCM

load-bearing objection Solid formal-methods paper that actually ships a usable representation and tool sketch for resource analysis of hybrid quantum programs with unbounded loops; the invariant caveat is real but already owned by the authors. the 2 major comments →

arxiv 2607.08548 v1 pith:USOOGZCM submitted 2026-07-09 quant-ph cs.PL

An Effective Quantum Hoare Logic for Hybrid Quantum Programs with Unbounded Loops

Christophe Chareton , Jad Issa , Romain P\'echoux This is my paper
classification quant-ph cs.PL
keywords quantum Hoare logichybrid quantum programsunbounded loopspath-sumsinteger hybrid path-sumsresource analysisalmost-sure terminationsymbolic execution
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.

Hybrid quantum programs with unbounded loops (for example repeat-until-success) are becoming common, yet existing tools either cannot handle unbounded recursion or cannot scale beyond matrix-level reasoning. This paper introduces integer hybrid path-sums (IHPS), a compact symbolic representation of hybrid quantum-classical states that can describe infinite supports arising from while loops. It builds a sound, non-branching quantum Hoare logic on IHPS together with a Collect heuristic that produces loop invariants from which almost-sure termination, expected runtime, and other costs can be read off. A Haskell prototype performs the forward symbolic execution and raises the remaining equivalence obligations. If the approach works, designers of near-term quantum software obtain exact resource estimates without full simulation, which matters while hardware remains scarce.

Core claim

The paper establishes the first semi-automated static analysis that simultaneously performs effective functional verification and resource (termination or cost) estimation for hybrid quantum programs with unbounded while loops. The vehicle is integer hybrid path-sums (IHPS), which extend ordinary path-sums with integer variables, infinite binders and limits; these serve as the predicates of a sound non-branching Hoare logic whose While rule is discharged by a Collect invariant heuristic that yields a limiting IHPS from which termination probability and expected resource consumption follow.

What carries the argument

Integer hybrid path-sums (IHPS): symbolic sums that encode quantum superpositions, classical probabilistic branching, integer counters and iteration limits; they act as compact predicates in a non-branching quantum Hoare logic whose loop rule is made practical by the Collect heuristic.

Load-bearing premise

Useful closed-form loop invariants of the special Collect shape must exist and be supplied by the user for the programs of interest, even though both equivalence checking and Hoare-triple validity are undecidable in general.

What would settle it

Produce a hybrid quantum program with an unbounded while loop for which no Collect-shaped IHPS is a valid invariant, or for which the resource expectations derived from the limiting IHPS disagree with direct simulation on a small concrete instance; or exhibit a counter-example to the soundness of the logic or equational theory on a loop-free fragment.

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

If this is right

  • Repeat-until-success patterns (unitary synthesis, Bernoulli factories, weak measurements) can have almost-sure termination and expected iteration counts extracted symbolically rather than by simulation.
  • Nested hybrid loops whose outer success probability depends on the inner-loop iteration count become analyzable without computing hard real or complex limits by hand.
  • Any resource of interest (T-gate count, multi-qubit gates, runtime) can be instrumented as a classical integer counter whose expectation is read from the limiting IHPS.
  • Black-box unitaries outside the fixed gate set can be treated by axiomatic Hoare triples, so the method is not limited to Clifford+R_k.
  • A complete static resource-analysis tool for hybrid quantum programs becomes a realistic engineering target once IHPS equivalence proofs are mechanized.

Where Pith is reading between the lines

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

  • If Collect-style invariants prove reusable, the same technique could certify average-case gate counts for fault-tolerant state-preparation routines that rely on repeated measurement and post-selection.
  • Mechanizing the remaining IHPS equivalence obligations (currently only float-checked) would turn the prototype into a practical companion for algorithm designers who must budget scarce hardware.
  • Because full automation is blocked by undecidability, practical success will likely rest on libraries of domain-specific invariant templates rather than free-form discovery.
  • The approach suggests a hybrid of classical probabilistic-program expectation transformers with path-sum fidelity, potentially importing automation techniques while retaining exact quantum branching structure.

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

2 major / 5 minor

Summary. The paper introduces HQbricks∞ (hybrid programs with unbounded while loops and integer computation) and integer hybrid path-sums (IHPS) as a symbolic representation of CQ states. It defines a non-branching quantum Hoare logic over IHPS, an equational theory, and the Collect heuristic for loop invariants of a particular shape, from which almost-sure termination and expected resource costs can be read off. Soundness is proved relative to a denotational CQ-state semantics (Theorems 4.3–4.4, 5.1); adequacy holds on the loop-free fragment (Theorem 4.6). Undecidability of equivalence and triple validity is stated (Theorem 4.2). A Haskell prototype IHPSlib performs forward symbolic execution and floating-point semantic sanity checks on the resulting obligations. Case studies include RUS unitary synthesis, QBF, weak measurements, and a nested-loop example.

Significance. If the results hold, the work fills a genuine gap between compact path-sum style symbolic execution (previously limited to bounded/hybrid-but-not-unbounded programs) and quantum Hoare logics that support unbounded hybrid control but lack effective equational reasoning. The combination of functional postconditions with resource extraction (termination probability, expected iteration/gate counts) via a single IHPS invariant is practically useful for near-term hybrid algorithms. Explicit strengths include machine-checkable soundness relative to an independent density-operator semantics, an admissible Collect rule with a clear proof, a working semi-automated implementation, and non-trivial examples (including nested communicating loops). The paper is appropriately modest about incompleteness and Π⁰₁-hardness.

major comments (2)
  1. Central claim (Abstract; §1.2 contributions 4–5; §7): the work is presented as the first semi-automated solution combining functional verification and resource estimation. In §7 the tool only raises proof obligations and performs floating-point CQ sanity checks (tolerance 1e-15, free integers 0..100); full discharge of IHPS equivalences and invariant conservation is left to future work. Given Theorem 4.2 (Π⁰₁-hardness) and Theorem 4.6 (adequacy only loop-free), the manuscript should more sharply delimit what is currently automated versus what remains user-supplied, so that the “semi-automated / effective” claim is not overstated relative to the implemented artifact.
  2. §5, Theorem 5.1 (Collect): the heuristic produces invariants of a fixed one-sided branching shape. The paper correctly notes that closed-form invariants need not exist in general, yet the resource-analysis pipeline and all case studies rely on this shape. A short discussion of the class of programs for which Collect-shaped invariants are expected to exist (or a counter-example sketch where they fail) would make the scope of the resource-estimation claims more precise and load-bearing.
minor comments (5)
  1. §4.2: the equational theory is only sketched (inherited HQbricks rules plus a few limit rules). A compact table or appendix listing the full set of rules used by IHPSlib would improve reproducibility.
  2. §6.2 Nested: the example is explicitly ad-hoc. A sentence clarifying that it is a stress test of expressiveness rather than a realistic algorithm would help readers calibrate expectations.
  3. Notation: the distinction between addresses (typewriter) and path variables (italic) is useful but occasionally blurred in prose; a short reminder early in §3 would help.
  4. Fig. 5 derivation of Synth: several intermediate rewrites (CV, Phase-Elim, cosine simplification) are named but not formally justified in the main text; a pointer to the corresponding equational rules would aid checking.
  5. Typos / polish: “path-susm” (Def. 3.2), “Adeqacy” (Thm 4.6 title), occasional missing spaces around math. Minor but easy to clean.

Circularity Check

1 steps flagged

No significant circularity: formal construction with independent denotational soundness; HQbricks self-citation is representational inheritance, not a load-bearing definition of the new unbounded-loop results.

specific steps
  1. self citation load bearing [§1.2 Contributions (2); §3; §4.2; comparison paragraph after Def. 3.2]
    "We further extend this formalism to integer HPS (IHPS), which include variables and constructs for handling integers. ... IHPS are an extension of the HPS from HQbricks for use in the analysis of unbounded loops. ... We enrich and adapt the equational theories from the HPS formalism introduced in HQbricks [18] to the IHPS formalism ... As for the rules inherited from the HPS formalism in HQbricks [18], we do not reprove them and refer the reader to that article for details."

    HQbricks is prior work by overlapping authors (Chareton, Issa et al.). The present paper inherits the base hybrid path-sum representation and some equational rules without re-proving them. This is ordinary incremental research, not a circular definition of the new unbounded results (lim, Collect, resource extraction, soundness of While). The load-bearing soundness (Thm 4.4) is established directly against the independent CQ denotational semantics, so the self-citation is not load-bearing for the central claim.

full rationale

This is a self-contained formal-methods paper. The core claims (IHPS representation, non-branching Hoare logic of Fig. 4, soundness Thm 4.4 w.r.t. the independent CQ-state denotational semantics of Fig. 3, admissible Collect heuristic Thm 5.1, and IHPSlib) are derived by structural induction and equational rewriting; they do not reduce by construction to fitted parameters or to a self-defined quantity. The only self-citation of note is the inheritance of the HPS base (and some equational rules) from HQbricks [18] (overlapping authors). That citation supplies the bounded hybrid case; the present paper’s novelty (integer binders, lim, While rule, Collect, resource extraction via norms of limit IHPS, nested-loop example) is independent and proven relative to the new denotational semantics. Equivalence and triple validity are explicitly Π⁰₁-hard (Thm 4.2) and adequacy holds only for loop-free programs (Thm 4.6); the tool only performs floating-point sanity checks. These are incompleteness caveats, not circular reductions. No fitted-input-as-prediction, uniqueness-from-authors, ansatz-smuggling, or renaming-of-known-result patterns appear. Score 1 reflects one non-load-bearing self-citation of prior representation work.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 3 invented entities

The paper rests on standard quantum information (Hilbert/Fock spaces, CQ states, dephasing, superoperators) and on the path-sum tradition. The main invented objects are the IHPS syntax/semantics and the HQbricks∞ language. No numerical free parameters are fitted to experimental data; resource numbers (e.g. E[x]=4/3 for Synth) are derived from the symbolic invariants. Completeness is deliberately sacrificed to undecidability.

axioms (4)
  • domain assumption Standard CQ-state denotational semantics of hybrid quantum programs (density operators, dephasing of classical registers, while as limit of filtered iterates).
    Foundation of soundness (Fig. 3, Def. 2.3, Prop. 2.5); standard in quantum programming literature.
  • domain assumption Path-sum / hybrid path-sum equational theory fragments (interfere, algebraic, world-combination rules) remain sound when lifted to IHPS.
    Inherited from Amy and HQbricks; new limit rules require separate convergence conditions (Thm. 4.3).
  • domain assumption Clifford+R_k gate set is pseudo-universal and admits exact dyadic/constructible phase-norm terms in IHPS.
    §2.1; other unitaries handled as black-box axioms in Δ (e.g. U_p in QBF).
  • ad hoc to paper Useful closed-form IHPS invariants of Collect shape exist for the target programs; remaining equivalences are checkable by user or future solvers.
    Required by While/Collect and by the semi-automated workflow; undecidability (Thm. 4.2) makes this an operational assumption, not a theorem.
invented entities (3)
  • Integer hybrid path-sums (IHPS) no independent evidence
    purpose: Compact symbolic representation of infinite-support CQ states for unbounded hybrid programs, supporting equational rewriting and resource extraction.
    Core technical invention (Def. 3.2); extends HPS with integers, lim/Σ/N binders, and ⊕.
  • HQbricks∞ language no independent evidence
    purpose: Imperative hybrid language with qubits, bits, integers, measure, and unbounded while, as the object of analysis.
    Defined in Fig. 2; variant of HQbricks with unbounded recursion and integer computation.
  • IHPSlib semi-automated engine no independent evidence
    purpose: Forward symbolic execution of the Hoare rules with invariant annotations and semantic equivalence checks.
    §7 implementation contribution; proof obligations left for future mechanization.

pith-pipeline@v1.1.0-grok45 · 53370 in / 3056 out tokens · 33527 ms · 2026-07-10T05:33:39.353040+00:00 · methodology

0 comments
read the original abstract

While quantum hardware remains limited, hybrid quantum-classical algorithms with complex control structures, including unbounded loops, are emerging, posing new challenges for quantum program analysis, including the accurate estimation of the resource consumption of a given program. Meanwhile, precise analysis techniques such as symbolic execution have largely left out hybridization and unbounded recursion. On the other hand, current quantum Hoare logics that generally support them are lacking in expressiveness and miss out on efficient computational equational reasoning that could be implemented in a semi-automated tool. This leaves a gap awaiting to be filled. In this work, we answer this challenge with the first semi-automated static analysis solution combining effective functional verification and resource (termination or cost) estimation for hybrid quantum programs with unbounded loops. Towards that end, we introduce integer hybrid path-sums (IHPS), extending path-sums to handle unbounded while loops, as a representation of possible executions of a program. A generic strategy for determining termination and expected resource consumption via loop invariants is also proposed and illustrated on several examples. Finally, the solution is implemented as a semi-automatic Haskell program. This work is the first step toward the design of a complete static resource analysis tool for hybrid quantum programs, essential for the development of real-world quantum computing.

Figures

Figures reproduced from arXiv: 2607.08548 by Christophe Chareton, Jad Issa, Romain P\'echoux.

Figure 1
Figure 1. Figure 1: The circuit for the RUS unitary synthesis of [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Syntax of HQbricks∞ HQbricks∞ is flexible on the choice of the supported unitaries, but in this article, we fix1 U ∈ {CNOT, X, Z, H} ∪ {R𝑘 = RZ( 2𝜋 2 𝑘 ) | 𝑘 ∈ N} which lends itself well to symbolic representations in terms of path-sums (§ 3) while remaining pseudo-universal; i.e., capable of approximating any unitary with arbitrary precision [26]. Well-formedness. The programs of HQbricks∞ are subject to … view at source ↗
Figure 3
Figure 3. Figure 3: Denotational Semantics of Hybrid Quantum Programs [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Hoare logic rules for IHPS. form of an IHPS with a free integer variable 𝑥 representing the iteration number of the loop. The limiting behavior of the loop is then captured by filtering out the non-exiting states and pushing 𝑥 to infinity. Example 4.1. We illustrate our logic in [PITH_FULL_IMAGE:figures/full_fig_p015_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Derivation of the first iteration of the loop in Listing [PITH_FULL_IMAGE:figures/full_fig_p021_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Output of IHPS on the annotated source code coin-toss.hyq of CoinToss. addresses are assigned to 0 is generated. For CoinToss, 𝔰 = ∅ and ℎ0 = ⟨0, 1 · ∅⟩. The tool is then able to compute the IHPS ℎ and a set of equivalences Ξ such that |= ⊢ {ℎ0} p {ℎ} by forward application of the logic rules of [PITH_FULL_IMAGE:figures/full_fig_p025_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Memory behavior of programs and the judgement [PITH_FULL_IMAGE:figures/full_fig_p029_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Interpretation of terms under variable assignment environments [PITH_FULL_IMAGE:figures/full_fig_p030_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: The functions b ∗ ℎ and ℎ[𝑎 ← 𝑡] applied to ℎ rewritten as red⊗ (ℎ) Certain desired algebraic rules, such as the one saying that if ℎ1 ≡ ℎ ′ 1 and ℎ2 ≡ ℎ ′ 2 , then ℎ1 + ℎ2 ≡ ℎ ′ 1 + ℎ ′ 2 , are not technically sound for the equivalence introduced since erasable phases global to ℎ1 and ℎ2 become relative in ℎ1 + ℎ2. Therefore, there is a need to define a stronger equivalence relation ≡𝑠 for which Γ |= ℎ1 ≡… view at source ↗
Figure 10
Figure 10. Figure 10: ⊗-reduced form red⊗ (ℎ) of an IHPS ℎ [PITH_FULL_IMAGE:figures/full_fig_p032_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: The inductive definition of evℎ(·) evaluating boolean b and integer i values within the environment ℎ. A.4 Hoare-style rules for unitaries apply(U)(ℎ1 + ℎ2) def = apply(U)(ℎ1) + apply(U)(ℎ2) apply(U)(ℎ1 ⊕ ℎ2) def = apply(U)(ℎ1) ⊕ apply(U)(ℎ2) apply(U)(ℎ1 ⊗ ℎ2) def = apply(U)(ℎ1) ⊗ ℎ2 if 𝔰(ℎ2) = ∅ apply(U)(ℎ1 ⊗ ℎ2) def = ℎ1 ⊗ apply(U)(ℎ2) if 𝔰(ℎ1) = ∅ apply(U) ∑︁ 𝑥 ℎ  def = ∑︁ 𝑥 apply(U)(ℎ) apply(U)  li… view at source ↗
Figure 12
Figure 12. Figure 12: Definition of apply(U)(ℎ) given for ℎ rewritten in ⊗-reduced form ℎ ↦→ red⊗ (ℎ) Unitary gates are applied again as symbolic transformations of IHPS terms. We define them inductively on IHPS in general, and for each unitary gate, we define its effect on primitive IHPS terms. They are given in [PITH_FULL_IMAGE:figures/full_fig_p033_12.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

70 extracted references · 70 canonical work pages · 7 internal anchors

  1. [1]

    Proceedings of the ACM on Programming Languages9(POPL), 923–953 (2025)

    Abdulla, P.A., Chen, Y.G., Chen, Y.F., Holík, L., Lengál, O., Lin, J.A., Lo, F.Y., Tsai, W.L.: Verifying quantum circuits with level-synchronized tree automata. Proceedings of the ACM on Programming Languages9(POPL), 923–953 (2025)

    work page 2025

  2. [2]

    Proceedings of the ACM on Programming Languages10(POPL), 2021–2050 (2026)

    Abdulla, P.A., Chen, Y.F., Hečko, M., Holík, L., Lengál, O., Lin, J.A., Thinniyam, R.S.: Parameterized verification of quantum circuits. Proceedings of the ACM on Programming Languages10(POPL), 2021–2050 (2026)

    work page 2021

  3. [3]

    In: Proceedings 15th International Conference on Quantum Physics and Logic, QPL 2018, Halifax, Canada, 3-7th June 2018

    Amy, M.: Towards large-scale functional verification of universal quantum circuits. In: Proceedings 15th International Conference on Quantum Physics and Logic, QPL 2018, Halifax, Canada, 3-7th June 2018. EPTCS, vol. 287, pp. 1–21 (2018). https://doi.org/10.4204/EPTCS.287.1

    work page doi:10.4204/eptcs.287.1 2018

  4. [4]

    Complete Equational Theories for the Sum-Over-Paths with Unbalanced Amplitudes

    Amy, M.: Complete equational theories for the sum-over-paths with unbalanced amplitudes. arXiv preprint arXiv:2306.16369 (2023)

    work page internal anchor Pith review Pith/arXiv arXiv 2023

  5. [5]

    Amy, M., Lunderville, J.: Linear and non-linear relational analyses for quantum program optimization. Proc. ACM Program. Lang.9(POPL), 1072–1103 (2025). https://doi.org/10.1145/3704873

    work page doi:10.1145/3704873 2025

  6. [6]

    Quantum Science and Technology7(2), 025007 (2022)

    Andrés-Martínez, P., Heunen, C.: Weakly measured while loops: peeking at quantum states. Quantum Science and Technology7(2), 025007 (2022)

    work page 2022

  7. [7]

    14577, pp

    Avanzini, M., Moser, G., Péchoux, R., Perdrix, S.: On the Hardness of Analyzing Quantum Programs Quantitatively, Lecture Notes in Computer Science, vol. 14577, pp. 31–58. Springer (2024). https://doi.org/10.1007/978-3-031-57267-8_2

    work page doi:10.1007/978-3-031-57267-8_2 2024

  8. [8]

    In: Baier, C., Fisman, D

    Avanzini, M., Moser, G., Péchoux, R., Perdrix, S., Zamdzhiev, V.: Quantum expectation transformers for cost analysis. In: Baier, C., Fisman, D. (eds.) LICS. pp. 10:1–10:13. ACM (2022). https://doi.org/10.1145/3531130.3533332

    work page doi:10.1145/3531130.3533332 2022

  9. [9]

    Azure-Quantum-Content: What is the Azure Quantum Resource Estimator? (Jul 2024), https://learn.microsoft.com/en- us/azure/quantum/intro-to-resource-estimation

    work page 2024

  10. [10]

    In: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

    Barthe, G., Gao, M., Wang, T., Zhou, L.: Complete quantum relational hoare logics from optimal transport duality. In: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 884–925. IEEE (2025)

    work page 2025

  11. [11]

    In: TACAS

    Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C.: Probabilistic program verification via inductive synthesis of inductive invariants. In: TACAS. Lecture Notes in Computer Science, vol. 13994, pp. 410–429. Springer (2023)

    work page 2023

  12. [12]

    In: Chechik, M., Katoen, J.P., Leucker, M

    Bauer-Marquart, F., Leue, S., Schilling, C.: symQV: Automated symbolic verification of quantum programs. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) Formal Methods. pp. 181–198. Springer International Publishing, Cham (2023)

    work page 2023

  13. [13]

    International Journal of Theoretical Physics21(3), 177–201 (1982)

    Benioff, P.A.: Quantum mechanical Hamiltonian models of discrete processes that erase their own histories: Application to Turing machines. International Journal of Theoretical Physics21(3), 177–201 (1982)

    work page 1982

  14. [14]

    Assessing requirements to scale to practical quantum advantage

    Beverland, M.E., Murali, P., Troyer, M., Svore, K.M., Hoefler, T., Kliuchnikov, V., Low, G.H., Soeken, M., Sundaram, A., Vaschillo, A.: Assessing requirements to scale to practical quantum advantage. arXiv preprint arXiv:2211.07629 (2022)

    work page internal anchor Pith review Pith/arXiv arXiv 2022

  15. [15]

    Bocharov, A., Roetteler, M., Svore, K.M.: Efficient synthesis of universal repeat-until-success quantum circuits. Phys. Rev. Lett.114, 080502 (Feb 2015). https://doi.org/10.1103/PhysRevLett.114.080502, https://link.aps.org/doi/10.1103/ PhysRevLett.114.080502

    work page doi:10.1103/physrevlett.114.080502 2015

  16. [16]

    Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: RTA. pp. 323–337. Springer (2005)

    work page 2005

  17. [17]

    In: Yoshida, N

    Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verification framework for circuit- building quantum programs. In: Yoshida, N. (ed.) ESOP 2021. Lecture Notes in Computer Science, vol. 12648, pp. 148–177. Springer (2021). https://doi.org/10.1007/978-3-030-72019-3_6

    work page doi:10.1007/978-3-030-72019-3_6 2021

  18. [18]

    Proceedings of the ACM on Programming Languages10, 1687–1713 (6 2026)

    Chareton, C., Issa, J., Nguyen, M., Blanco, N., Bardin, S.: Hybrid path-sums for hybrid quantum programs. Proceedings of the ACM on Programming Languages10, 1687–1713 (6 2026). https://doi.org/10.1145/3808314, https://doi.org/10. 1145/3808314

    work page doi:10.1145/3808314 2026

  19. [19]

    In: Akleylek, S., Dundua, B

    Chareton, C., Lee, D., Valiron, B., Vilmart, R., Bardin, S., Xu, Z.: Formal methods for quantum algorithms. In: Akleylek, S., Dundua, B. (eds.) Handbook of Formal Analysis and Verification in Cryptography, pp. 319–422. CRC Press (2023). https://doi.org/10.1201/9781003090052-7

    work page doi:10.1201/9781003090052-7 2023

  20. [20]

    Proceedings of the ACM on Programming Languages9(OOPSLA2), 2981–3007 (2025)

    Cheng, F., Vangeepuram, S., Allard, H., Jafari, S.M.R., Potanin, A., Li, L.: Embedding quantum program ver- ification into dafny. Proceedings of the ACM on Programming Languages9(OOPSLA2), 2981–3007 (2025). https://doi.org/https://doi.org/10.1145/3763157

    work page doi:10.1145/3763157 2025

  21. [21]

    New Journal of Physics13(4), 043016 (2011) An Effective Quantum Hoare Logic for Hybrid Quantum Programs with Unbounded Loops 27

    Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New Journal of Physics13(4), 043016 (2011) An Effective Quantum Hoare Logic for Hybrid Quantum Programs with Unbounded Loops 27

    work page 2011

  22. [22]

    In: International conference on theory and application of diagrams

    Coecke, B., Kissinger, A.: Picturing quantum processes: A first course on quantum theory and diagrammatic reasoning. In: International conference on theory and application of diagrams. pp. 28–31. Springer (2018)

    work page 2018

  23. [23]

    In: ESOP 2024

    Colledan, A., Lago, U.D.: Circuit width estimation via effect typing and linear dependency. In: ESOP 2024. Lecture Notes in Computer Science, vol. 14577, pp. 3–30. Springer (2024). https://doi.org/10.1007/978-3-031-57267-8_1

    work page doi:10.1007/978-3-031-57267-8_1 2024

  24. [24]

    Proceedings of the ACM on Programming Languages9(POPL), 1386–1416 (2025)

    Colledan, A., Lago, U.D.: Flexible type-based resource estimation in quantum circuit description languages. Proceedings of the ACM on Programming Languages9(POPL), 1386–1416 (2025). https://doi.org/10.1145/3704883

    work page doi:10.1145/3704883 2025

  25. [25]

    In: Abdulla, P.A., Kesner, D

    Dave, K., Lemonnier, L., Péchoux, R., Zamdzhiev, V.: Combining quantum and classical control: syntax, semantics and adequacy. In: Abdulla, P.A., Kesner, D. (eds.) FoSSaCS 2025. Lecture Notes in Computer Science, vol. 15691, pp. 155–175. Springer (2025). https://doi.org/10.1007/978-3-031-90897-2_8

    work page doi:10.1007/978-3-031-90897-2_8 2025

  26. [26]

    Proceedings of the Royal Society of London

    Deutsch, D.E., Barenco, A., Ekert, A.: Universality in quantum computation. Proceedings of the Royal Society of London. Series A: Mathematical and Physical Sciences449(1937), 669–677 (1995)

    work page 1937

  27. [27]

    ACM Transactions on Quantum Computing2(4), 1–43 (2021)

    Feng, Y., Ying, M.: Quantum Hoare logic with classical variables. ACM Transactions on Quantum Computing2(4), 1–43 (2021)

    work page 2021

  28. [28]

    Feynman, R.P.: Space-time approach to non-relativistic quantum mechanics. Rev. Mod. Phys.20, 367–387 (1948). https://doi.org/10.1103/RevModPhys.20.367

    work page doi:10.1103/revmodphys.20.367 1948

  29. [29]

    Zeitschrift für Physik75(9), 622–647 (1932)

    Fock, V.: Konfigurationsraum und zweite Quantelung. Zeitschrift für Physik75(9), 622–647 (1932)

    work page 1932

  30. [30]

    In: International Conference on Reversible Computation

    Fu, P., Kishida, K., Ross, N.J., Selinger, P.: A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper. In: International Conference on Reversible Computation. pp. 153–168. Springer (2020)

    work page 2020

  31. [31]

    Quantum8, 1423 (2024)

    de Gliniasty, G., Hilaire, P., Emeriau, P.E., Wein, S.C., Salavrakos, A., Mansfield, S.: A spin-optical quantum computing architecture. Quantum8, 1423 (2024)

    work page 2024

  32. [32]

    Nature638(8052), 920–926 (2025)

    Google Quantum AI and Collaborators: Quantum error correction below the surface code threshold. Nature638(8052), 920–926 (2025)

    work page 2025

  33. [33]

    In: FoSSaCS

    Hainry, E., Péchoux, R., Silva, M.: A programming language characterizing quantum polynomial time. In: FoSSaCS

    work page

  34. [34]

    13992, pp

    Lecture Notes in Computer Science, vol. 13992, pp. 156–175. Springer (2023). https://doi.org/10.1007/978-3-031- 30829-1_8

    work page doi:10.1007/978-3-031- 2023

  35. [35]

    In: Fernández, M

    Hainry, E., Péchoux, R., Silva, M.: Branch sequentialization in quantum polytime. In: Fernández, M. (ed.) FSCD 2025. LIPIcs, vol. 337, pp. 22:1–22:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2025). https://doi.org/10.4230/LIPICS.FSCD.2025.22

    work page doi:10.4230/lipics.fscd.2025.22 2025

  36. [36]

    In: Cohen, L., Kaliszyk, C

    Hietala, K., Rand, R., Hung, S.H., Li, L., Hicks, M.: Proving Quantum Programs Correct. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 193, pp. 21:1–21:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2021)....

    work page doi:10.4230/lipics.itp.2021.21 2021

  37. [37]

    In: Thiemann, P

    Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run–times of probabilistic programs. In: Thiemann, P. (ed.) Programming Languages and Systems. pp. 364–389. Springer Berlin Heidelberg, Berlin, Heidelberg (2016)

    work page 2016

  38. [38]

    In: 38th European Conference on Object-Oriented Programming (ECOOP 2024)

    Li, L., Zhu, M., Cleaveland, R., Nicolellis, A., Lee, Y., Chang, L., Wu, X.: Qafny: A quantum-program verifier. In: 38th European Conference on Object-Oriented Programming (ECOOP 2024). pp. 24–1. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2024). https://doi.org/https://doi.org/10.4230/LIPIcs.ECOOP.2024.24

    work page doi:10.4230/lipics.ecoop.2024.24 2024

  39. [39]

    Physical Review A—Atomic, Molecular, and Optical Physics73(1), 012304 (2006)

    Lim, Y.L., Barrett, S.D., Beige, A., Kok, P., Kwek, L.C.: Repeat-until-success quantum computing using stationary and flying qubits. Physical Review A—Atomic, Molecular, and Optical Physics73(1), 012304 (2006)

    work page 2006

  40. [40]

    Lim, Y.L., Beige, A., Kwek, L.C.: Repeat-until-success linear optics distributed quantum computing. Phys. Rev. Lett. 95, 030505 (Jul 2005). https://doi.org/10.1103/PhysRevLett.95.030505, https://link.aps.org/doi/10.1103/PhysRevLett.95. 030505

    work page doi:10.1103/physrevlett.95.030505 2005

  41. [41]

    A Game of Surface Codes: Large-Scale Quantum Computing with Lattice Surgery

    Litinski, D.: A game of surface codes: Large-scale quantum computing with lattice surgery. arXiv preprint arXiv:1808.02892 (Aug 2018). https://doi.org/10.22331/q-2019-03-05-128, http://arxiv.org/abs/1808.02892v3, quantum 3, 128 (2019)

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.22331/q-2019-03-05-128 2018

  42. [42]

    In: International conference on computer aided verification

    Liu, J., Zhan, B., Wang, S., Ying, S., Liu, T., Li, Y., Ying, M., Zhan, N.: Formal verification of quantum algorithms using quantum hoare logic. In: International conference on computer aided verification. pp. 187–207. Springer (2019)

    work page 2019

  43. [43]

    In: Baier, C., Fisman, D

    Liu, J., Zhou, L., Barthe, G., Ying, M.: Quantum weakest preconditions for reasoning about expected runtimes of quantum programs. In: Baier, C., Fisman, D. (eds.) LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022. pp. 4:1–4:13. ACM (2022). https://doi.org/10.1145/3531130.3533327

    work page doi:10.1145/3531130.3533327 2022

  44. [44]

    Journal of the ACM (5 2025)

    Liu, J., Zhou, L., Barthe, G., Ying, M.: Quantum weakest preconditions for reasoning about expected runtimes of quantum programs. Journal of the ACM (5 2025). https://doi.org/10.1145/3734516, https://doi.org/10.1145/3734516

    work page doi:10.1145/3734516 2025

  45. [45]

    In: 2019 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

    Meuli, G., Soeken, M., Campbell, E., Roetteler, M., de Micheli, G.: The role of multiplicative complexity in compiling low T-count oracle circuits. In: 2019 IEEE/ACM International Conference on Computer-Aided Design (ICCAD). pp. 1–8 (2019). https://doi.org/10.1109/ICCAD45719.2019.8942093 28 Jad Issa, Christophe Chareton, and Romain Péchoux

    work page doi:10.1109/iccad45719.2019.8942093 2019

  46. [46]

    Classical simulation of quantum computation, the Gottesman-Knill theorem, and slightly beyond

    Nest, M.: Classical simulation of quantum computation, the Gottesman-Knill theorem, and slightly beyond. arXiv preprint arXiv:0811.0898 (2008)

    work page internal anchor Pith review Pith/arXiv arXiv 2008

  47. [47]

    In: International Conference on Computer Aided Verification

    Novozhilov, S., Yang, M., Chen, M., Li, Z., Yin, J.: On the almost-sure termination of probabilistic counter programs. In: International Conference on Computer Aided Verification. pp. 82–104. Springer (2025)

    work page 2025

  48. [48]

    Repeat-Until-Success: Non-deterministic decomposition of single-qubit unitaries

    Paetznick, A., Svore, K.M.: Repeat-until-success: Non-deterministic decomposition of single-qubit unitaries. arXiv preprint arXiv:1311.1074 (2013)

    work page internal anchor Pith review Pith/arXiv arXiv 2013

  49. [49]

    (Implicit Computational Complexity: past and future)

    Péchoux, R.: Complexité implicite : bilan et perspectives. (Implicit Computational Complexity: past and future). Université de Lorraine (2020), https://tel.archives-ouvertes.fr/tel-02978986

    work page 2020

  50. [50]

    In: Proceedings 35th Annual Symposium on Foundations of Computer Science

    Shor, P.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proceedings 35th Annual Symposium on Foundations of Computer Science. pp. 124–134 (1994). https://doi.org/10.1109/SFCS.1994.365700

    work page doi:10.1109/sfcs.1994.365700 1994

  51. [51]

    Proceedings of the ACM on Programming Languages10(POPL), 444–475 (2026)

    Su, B., Feng, Y., Ying, M., Zhou, L.: An expressive assertion language for quantum programs. Proceedings of the ACM on Programming Languages10(POPL), 444–475 (2026)

    work page 2026

  52. [52]

    Proceedings of the ACM on Programming Languages3(POPL), 1–31 (2019)

    Unruh, D.: Quantum relational Hoare logic. Proceedings of the ACM on Programming Languages3(POPL), 1–31 (2019)

    work page 2019

  53. [53]

    Quantum9, 1860 (Sep 2025)

    Vandaele, V.: Lower T-count with faster algorithms. Quantum9, 1860 (Sep 2025). https://doi.org/10.22331/q-2025-09- 16-1860, https://doi.org/10.22331/q-2025-09-16-1860

    work page doi:10.22331/q-2025-09- 2025

  54. [54]

    Vilmart, R.: Rewriting and completeness of sum-over-paths in dyadic fragments of quantum computing. Log. Methods Comput. Sci.20(1) (2024). https://doi.org/10.46298/LMCS-20(1:20)2024

    work page doi:10.46298/lmcs-20(1:20)2024 2024

  55. [55]

    Voichick, F., Li, L., Rand, R., Hicks, M.: Qunity: A unified language for quantum and classical computing. Proc. ACM Program. Lang.7(POPL), 921–951 (2023). https://doi.org/10.1145/3571225

    work page doi:10.1145/3571225 2023

  56. [56]

    arXiv preprint arXiv:2601.13313 (2026)

    Weilandt, E., Peham, T., Wille, R.: Synthesis of fault-tolerant state preparation circuits using steane-type error detection. arXiv preprint arXiv:2601.13313 (2026)

    work page arXiv 2026

  57. [57]

    Cambridge university press (2013)

    Wilde, M.: Quantum information theory. Cambridge university press (2013)

    work page 2013

  58. [58]

    Automating Equational Proofs in Dirac Notation

    Xu, Y., Barthe, G., Zhou, L.: Automating equational proofs in dirac notation. arXiv preprint arXiv:2411.11617 (2024). https://doi.org/https://doi.org/10.1145/3704878

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.1145/3704878 2024

  59. [59]

    Yamakami, T.: A schematic definition of quantum polynomial time computability. J. Symb. Log.85(4), 1546–1587 (2020). https://doi.org/10.1017/JSL.2020.45

    work page doi:10.1017/jsl.2020.45 2020

  60. [60]

    ACM Transactions on Programming Languages and Systems (TOPLAS)33(6), 1–49 (2012)

    Ying, M.: Floyd–hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS)33(6), 1–49 (2012)

    work page 2012

  61. [61]

    Elsevier (2024)

    Ying, M.: Foundations of quantum programming. Elsevier (2024). https://doi.org/10.1016/C2014-0-02660-3

    work page doi:10.1016/c2014-0-02660-3 2024

  62. [62]

    A Practical Quantum Hoare Logic with Classical Variables, I

    Ying, M.: A practical quantum Hoare logic with classical variables, I. CoRRabs/2412.09869(2024). https://doi.org/10.48550/ARXIV.2412.09869

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2412.09869 2024

  63. [63]

    Proceedings of the ACM on Programming Languages10(PLDI), 928–952 (2026)

    Yu, N., Palsberg, J., Reps, T.: Saqr-qc: a logic for scalable but approximate quantitative reasoning about quantum circuits. Proceedings of the ACM on Programming Languages10(PLDI), 928–952 (2026)

    work page 2026

  64. [64]

    Proceedings of the ACM on Programming Languages10(PLDI), 200–225 (2026)

    Yuan, C.: Cobble: Compiling block encodings for quantum computational linear algebra. Proceedings of the ACM on Programming Languages10(PLDI), 200–225 (2026)

    work page 2026

  65. [65]

    the program p is valid to be executed starting from a state with memory allocation profile 𝔰1 and will result in a state with memory allocation profile 𝔰2

    Zhou, L., Barthe, G., Strub, P., Liu, J., Ying, M.: CoqQ: Foundational verification of quantum programs. Proceedings of the ACM on Programming Languages7(POPL), 833–865 (2023). https://doi.org/10.1145/3571222 An Effective Quantum Hoare Logic for Hybrid Quantum Programs with Unbounded Loops 29 A Exhaustive formalism In this section of the appendix, we prov...

    work page doi:10.1145/3571222 2023

  66. [66]

    By induction on the second derivation, we have that𝔰(ℎ 2) =p 2(𝔰(ℎ′ 1))

    = p1(𝔰(ℎ1)). By induction on the second derivation, we have that𝔰(ℎ 2) =p 2(𝔰(ℎ′ 1)). As such,𝔰(ℎ 2) =p 2(p1(𝔰(ℎ1))) =p(𝔰(ℎ 1)). (3)Eqiv : There exists ℎ′ 2 such that ℎ2 ≡ℎ ′ 2 and {ℎ1} p ℎ′ 2 . By induction, we have that 𝔰(ℎ′

    work page

  67. [67]

    =p(𝔰(ℎ 1)), andℎ 2 ≡ℎ ′ 2, we have that𝔰(ℎ 2) =𝔰(ℎ ′

    work page

  68. [68]

    =p(𝔰(ℎ 1)). (4)Unitary , Assignb, Assigni, and Measure: These programs don’t affect signatures, so 𝔰(ℎ2) =𝔰(ℎ 1) =p(𝔰(ℎ 1)) (5)QInit: We havep=qubitq, andℎ 2 =ℎ 1 ⊗ |0⟩q, so that𝔰(ℎ 2) =𝔰(ℎ 1)∪ {q}=p(𝔰(ℎ 1)). (6)CInit: Similar toQInit, we have𝔰(ℎ 2) =𝔰(ℎ 1)∪ {c}=p(𝔰(ℎ 1)). (7)IntInit: Similar toQInit, we have𝔰(ℎ 2) =𝔰(ℎ 1)∪ {x}=p(𝔰(ℎ 1)). (8)If: The deriv...

    work page

  69. [69]

    As such,𝔰(ℎ 2) =𝔰(ℎ b

    = p1(𝔰(b∗ℎ 1)) = p1(𝔰(ℎ1))and 𝔰(ℎ¬b 2 ) = p2(𝔰((1 ⊕ b)∗ℎ 1)) =p 2(𝔰(ℎ1)). As such,𝔰(ℎ 2) =𝔰(ℎ b

    work page

  70. [70]

    =𝔰(ℎ ¬b 2 ) =p 1(𝔰(ℎ1)) =p 2(𝔰(ℎ1)) =p(𝔰(ℎ 1)). (9)While : By the assumption that the rules are applied on valid program/ IHPS pairs only, p = whilebdop ′ done does not affect signatures and neither does p′, so by the inductive hypothesis, we have that𝔰(ℎ 2) =𝔰(ℎ 1) =p(𝔰(ℎ 1)). As for (ii), we use Theorem 4.4 to write: JpK (cq(ℎ1)) = cq(ℎ 2) JpK (cq(ℎ3)) ...

    work page