Pith. sign in

REVIEW 4 major objections 4 minor 112 references

Continuous-variable quantum programs get a sound and complete Hoare logic

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 · deepseek-v4-flash

2026-08-01 03:29 UTC pith:OQGWYHMU

load-bearing objection First end-to-end cost-parametric Hoare logic for continuous-variable quantum programs with unbounded expectations; the architecture is convincing, but the completeness proof and the M-admissibility bridge live in the supplementary material, so acceptance should hinge on those. the 4 major comments →

arxiv 2607.23137 v1 pith:OQGWYHMU submitted 2026-07-25 cs.LO cs.PLmath.FAquant-ph

Reasoning about Continuous-Variable Quantum Systems

Tianshi Yu , Gilles Barthe , Minbo Gao , Mingsheng Ying , Li Zhou This is my paper
classification cs.LO cs.PLmath.FAquant-ph MSC 68Q6003B7081P68
keywords continuous-variable quantum computingquantum Hoare logicweakest preconditionsclosed positive quadratic formsunbounded quantum predicatescontinuous-outcome measurementGKP error correctionexpected cost
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.

This paper develops a cost-parametric quantum Hoare logic for continuous-variable quantum programs, where measurement outcomes are real numbers rather than discrete branches. It claims that for every well-formed admissible program, a Hoare triple is derivable exactly when it is semantically valid, for any base cost parameter. The key design choice is to use closed positive quadratic forms as predicates, which package finite expectations, finiteness domains, and infinite penalties in a single ordered structure that remains closed under weakest-precondition operations. Continuous measurement is handled by Bochner integration of measurable branch states, and the cost of a program itself becomes a closed positive form, so nontermination and infinite expected cost appear as ordinary predicate values rather than external side conditions. Two case studies demonstrate the power of this setup: a quantum symmetric walk separates almost-sure termination from finite expected cost, and a one-round GKP error-correction program yields a direct variance bound without any finite-dimensional cutoff.

Core claim

The paper establishes that the cost-parametric weakest-precondition calculus for an infinite-dimensional quantum while-language with continuous-outcome bind is sound and relatively complete (Theorems 5.2 and 5.3). For every admissible program S, closed positive quadratic-form predicates P and Q, and base cost c ≥ 0, ⊢_c {P} S {Q} holds if and only if |=_c {P} S {Q}, where validity means Tr(Pρ) ≥ Tr(Q JSK(ρ)) + C_c(S,ρ) for every partial density operator ρ. The weakest precondition has the exact structure wp_c(S,Q) = JSK†(Q) + C_{c,S}, with the Heisenberg dual computed at the level of quadratic forms and the cost predicate C_{c,S} itself a closed positive form. This makes continuous measureme

What carries the argument

The central object is the predicate domain P of closed positive quadratic forms, equivalently positive self-adjoint linear relations, ordered by the extended Löwner order and forming an ω-CPO. This domain carries the load-bearing constructions: the unbounded Heisenberg dual defined by pulling back forms through Kraus operators, the continuous-measurement transformer that integrates branch form values rather than unbounded operators, and the cost-parametric weakest precondition wp_c(S,Q) = JSK†(Q) + C_{c,S}. The language semantics itself rests on the admissible continuous-outcome bind, whose denotation is a Bochner integral of measurable families of continuation-applied branch states; admissi

Load-bearing premise

The continuous-outcome bind is well defined only when the admissibility conditions of Section 3.2 hold: the Kraus density must be jointly measurable, the integral of M†M must equal the identity, and the continuation's branch-state map must be Bochner integrable with trace-class values; if these fail, the integral defining bind and the form-level predicate transformer are undefined, and the paper defers the detailed verification of these measurability conditions to the support

What would settle it

Exhibit an admissible program satisfying the well-formedness rules for which the Bochner integral defining bind does not yield a positive trace-class operator, or find a semantically valid triple |=_c {P} S {Q} that admits no derivation in the proof system. Concretely for the GKP case study: check whether the identity R = ∫ M_x† P_x M_x dx holds as an equality of closed quadratic forms under the stated Gaussian kernel and finite-moment assumptions; if that integral diverges or the equality fails, the claimed variance bound collapses.

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

If this is right

  • Continuous-variable quantum protocols can be verified directly at the infinite-dimensional level, without imposing energy cutoffs or finite-dimensional approximations.
  • A Hoare proof of finite pre-expectation with positive cost entails almost-sure termination, because divergence is represented as an infinite predicate value rather than an external side condition.
  • The same predicate transformer separates qualitative termination from finite expected cost: the quantum symmetric walk terminates almost surely yet has infinite expected operational cost in the wp₁ calculus.
  • GKP-style error-correction programs are verifiable in the logic: one round of linearized correction proves the output second moment is bounded by σ_a² + σ_M² times the input trace.
  • Relative completeness means every semantically valid cost bound has a syntax-directed Hoare proof, enabling compositional verification of larger CV programs.

Where Pith is reading between the lines

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

  • The form-level integration technique likely extends to other outcome-indexed constructs, such as adaptive measurements or Bayesian updates, whenever the same joint measurability and Bochner-integrability conditions hold.
  • The GKP case study uses only the zero-cost fragment, suggesting the cost parameter can be tuned to trade termination obligations against physical resource bounds in other bosonic error-correction settings.
  • The variance bound for one-round correction is stated only for the linearized local regime; multi-round or nonlinear decoding would require composing round transformers and tracking higher moments, which the paper leaves open.
  • Since the paper defers detailed measurability proofs and the relative-completeness proof to supplementary material, mechanizing these proofs in a proof assistant would be a natural and demanding next step.

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 / 4 minor

Summary. The paper develops a cost-parametric quantum Hoare logic for continuous-variable quantum programs. States are partial density operators on separable Hilbert spaces; programs include an admissible continuous-outcome measurement bind interpreted by Bochner integration; predicates are closed positive quadratic forms, allowing unbounded expectations and hard constraints; the logic is claimed sound and relatively complete for validity defined by an extended trace inequality plus accumulated cost. Two case studies are given: a quantum symmetric random walk separating almost-sure termination from finite expected cost, and a one-round GKP correction proof of a second-moment bound.

Significance. If the central theorems hold, this is a substantial contribution: it is the first systematic cost-sensitive program logic for continuous-variable quantum programs with unbounded assertions. The choice of closed positive quadratic forms as predicates is well motivated, and the two case studies are well chosen: the random walk exhibits a genuine AST/infinite-cost separation, and the GKP proof demonstrates a direct variance bound without a finite-dimensional cutoff. The paper is also honest about the boundary between prior foundations and new results, and the visible algebraic calculations are coherent. However, the main meta-theorems rely on deferred measure-theoretic verifications, one of which is load-bearing for the completeness theorem.

major comments (4)
  1. [§4.3, Definition 4.2 and Theorem 5.3] The definition of the continuous-branch transformer requires the family {wlp(S_ν,Q)} to be M-admissible, and the completeness proof must instantiate the Bind rule with P_ν = wp_c(S_ν,Q). The main text asserts that the well-formedness and admissibility assumptions on bind ensure M-admissibility, but gives no argument. This is not a direct consequence of Theorem 3.1, which concerns trace-class denotations, not quadratic-form-valued pullbacks: one must prove that ν ↦ 𝔱_{wlp(S_ν,Q)}[M_ν u] is measurable and that the resulting form is closed. Since this assertion is the bridge between the forward semantics and the predicate calculus, it is load-bearing for Theorem 5.3 and for the Bind rule in Fig. 2. The proof must be supplied or the statement weakened.
  2. [§5.4, Theorems 5.2–5.3] The soundness and relative completeness theorems are the central claims of the paper, but their proofs are deferred entirely to the supplementary material. In particular, the completeness proof needs to show that the wp_c equations of Proposition 5.2 are well-defined for every admissible command, including the continuous bind and the while-loop supremum, and that every valid triple can be derived using the limited rule set of Fig. 2. Deferring these proofs is acceptable only if the supplementary material is complete and rigorous; as submitted, the main text gives only proof sketches and no route to checking the critical admissibility induction. Please state explicitly which parts of the completeness argument are established in the main text and ensure the supplementary proofs are available to the reviewers.
  3. [§7, Eq. (3) and Fig. 2] The GKP case study derives the Hoare triple for S_GKP ≡ A_GKP; U_SUM; B_hom, where A_GKP is an initialization to an approximate GKP state |φ_{Δ,κ}⟩. The syntax of Section 3.1 and the Init rule of Fig. 2 only provide q := |0⟩. The paper uses an initialization command with Kraus operators E_k = I_s ⊗ |φ⟩⟨k|, which is not an instance of the declared syntax or of the Init rule. If A_GKP is intended as a new primitive, the syntax and the rule set must be extended accordingly; otherwise the derivation of (3) is not an instance of the paper's own proof system.
  4. [§4.1–4.2, Theorem 4.1] The proof sketch of Theorem 4.1 says to approximate an unbounded postcondition by bounded positive operators, apply the bounded Heisenberg dual, and take the supremum. This requires justification that the resulting supremum does not depend on the approximating sequence and that the Kraus formula (1) is representation-independent even when the postcondition is unbounded. The appendix appears to address parts of this, but the main text should at least state the precise closure theorem used and point to the exact appendix section, since the trace duality is the foundation of all subsequent wlp equations.
minor comments (4)
  1. [Abstract and §3] Typo: 'omputational' should be 'computational'. Also, 'qadratic form' appears in the appendix headings; please fix the spelling.
  2. [§3.2, Section 3.3] The admissibility conditions for bind are presented informally; in particular, the normalization condition is written pointwise in u, but it should be stated clearly that this is a strong operator measurability condition on the raw product σ-algebra, not a completion condition. The appendix clarifies this, but the main text should mirror the formulation.
  3. [§7, Lemma 7.1] The proof of Lemma 7.1 is deferred to the supplementary material. The identities (4)–(7) are plausible and the visible calculation for (5) is correct, but since these equalities are the core of the GKP case study, a proof sketch in the main text would help the reader verify that the Gaussian integration and the Weyl relation are applied with the correct operator domains.
  4. [§6, Theorem 6.1] The random-walk proof distinguishes the wp0 computation as belonging to the bounded weakest-precondition calculus. This is a useful clarification, but the connection to the paper's own zero-cost fragment should be made precise: the reader needs to know whether wp0(while, I) = I is being derived from the soundness of Fig. 2 for c = 0 or from a prior bounded calculus, and why the two agree on this example.

Circularity Check

0 steps flagged

No substantive circularity: the central derivations are self-contained or reduce to ordinary algebra/measure theory. The only self-referential element is minor and non-load-bearing; the main-text M-admissibility bridge is a deferred proof, not a circular reduction.

full rationale

The paper's central claims do not reduce to their own inputs by construction. The predicate domain is initially credited to the authors' own prior work [5]: Section 4.1 says 'recent work [5] proposed using linear relations / closed quadratic forms as predicates. We follow this viewpoint' and recalls 'properties of this predicate domain, which are introduced in [5].' This is a genuine overlapping-author citation, which I flag as the reason the score is 2 rather than 0. However, it is not load-bearing in a circular way: Appendix A develops the linear-relation/quadratic-form machinery, Kato's representation theorem, monotone convergence, and the omega-CPO structure from scratch, and Appendix C proves the weakest-precondition structure and structural rules. The main-text proofs of Theorems 4.1 and Proposition 4.1 also give independent proof sketches. Thus the paper does not simply import its central logic from [5] by citation. The skeptic's M-admissibility concern is real but is not circularity. In Section 4.3 the paper asserts: 'The well-formedness and admissibility assumptions on bind ensure that the family {wlp(Sν,Q)}ν∈ΩM is M-admissible, so the integral defines a predicate in P(H).' This sentence is the bridge from Definition 4.2 to the Bind rule and to Theorem 5.3, and the main text defers the detailed proof to the supplementary material. That is an omitted/unverified lemma, i.e., a completeness gap if the supplementary proof fails, but it is not an equivalence-by-construction or fitted-input-as-prediction circular step. The GKP case study is a direct computation, not a fitted result: equations (4)-(7) of Lemma 7.1 follow from the Weyl displacement relation, joint functional calculus, and the first two Gaussian moments; the bound (σ_a^2+σ_M^2)Tr(ρ) is derived, not chosen to match the output. The random-walk case study likewise solves the wp0 and wp1 recurrence equations honestly and exhibits a genuine AST/infinite-cost separation. Finally, the soundness/completeness theorem uses the standard weakest-precondition route, and the proof rules mirror the structural clauses of wp_c; this is the normal structure of a compositional program logic, not a self-definitional collapse, because validity, wlp, cost, and completeness are stated as separate semantic and proof-theoretic objects and connected by proofs. Overall: no fitted parameter is renamed as a prediction, no uniqueness theorem from the authors is used to rule out alternatives, and no ansatz is smuggle

Axiom & Free-Parameter Ledger

3 free parameters · 7 axioms · 0 invented entities

The framework introduces no new physical entities or fitted constants. It relies on standard operator theory (Kato representation, monotone convergence, Kraus representation) and on explicit measurability/normalization admissibility assumptions for continuous instruments, plus the GKP local-regime assumptions for the case study.

free parameters (3)
  • Per-command base cost c = c≥0 (set to 1 in random walk)
    Parameter of the cost logic; not fitted to data. Affects validity semantics and the while rule.
  • Ancilla variance σ_a^2 = symbolic
    Input moment of the approximate GKP ancilla in Section 7; appears in the variance bound.
  • Measurement noise variance σ_M^2 = symbolic
    Variance of the Gaussian homodyne kernel; input parameter, not fitted.
axioms (7)
  • domain assumption All Hilbert spaces are separable and all measure spaces are σ-finite
    Section 2.1 and 2.3; needed for orthonormal bases, Bochner integrability, and product measures.
  • standard math Closed positive quadratic forms correspond bijectively to positive self-adjoint linear relations (Kato representation)
    Appendix A, Theorem A.2; foundational for the predicate domain.
  • standard math Monotone convergence for non-decreasing closed positive forms (ω-CPO property)
    Appendix A, Theorem A.3; used for loop semantics and wlp suprema.
  • standard math Every CPTN map has a countable Kraus representation with ∑K_m†K_m⊑I
    Appendix B, Theorem B.1; used for the wlp formula (Equation 1).
  • ad hoc to paper Program primitives satisfy strong measurability and normalization (admissible programs)
    Section 3.2 and Appendix B; this is the key semantic condition for continuous bind.
  • domain assumption GKP case study: ancilla has zero mean and finite variance σ_a^2; local regime with no lattice wrap-around and feedback r(x)=x
    Section 7; restricts the GKP variance bound to one-round linearized correction.
  • domain assumption Random-walk example: coin is reset each iteration so the position marginal is the classical symmetric walk
    Section 6; makes the null-recurrent separation transparent but is not a general logic axiom.

pith-pipeline@v1.3.0-alltime-deepseek · 65633 in / 21748 out tokens · 211492 ms · 2026-08-01T03:29:53.427554+00:00 · methodology

0 comments
read the original abstract

Continuous-variable quantum computing (CVQC) is a computing paradigm in which measurements yield values over a continuous domain. CVQC is both a convenient omputational framework for modeling physical quantum systems, and a good abstraction for hardware platforms based on quantum optics. Yet, the semantic foundations of CVQC remain underdeveloped. To address this gap, we develop a formal semantics for a core CV quantum programming language, and sound verification methods for program correctness. A main contribution of this work is to isolate a well-behaved quantitative predicate domain that achieves sufficient expressiveness to accommodate unbounded values as they arise in the infinite-dimensional, continuous setting. Specifically, we choose closed positive quadratic forms as semantic predicates, representing finite expectations, domains of finiteness, and infinite penalties in one ordered object. We validate our choice by establishing that our semantic predicates satisfy desirable closure properties including the definition of weakest preconditions. We validate our design with two case studies, including an example based on the celebrated GKP error-correcting code, for which we establish a second moment bound.

Figures

Figures reproduced from arXiv: 2607.23137 by Gilles Barthe, Li Zhou, Minbo Gao, Mingsheng Ying, Tianshi Yu.

Figure 1
Figure 1. Figure 1: Well-formedness The involved commands include unitary transformation, while loop and bind, since both 𝑈 and 𝑀 are parameterized. For a unitary command 𝑞 := 𝑈 [𝑞], it is admissible if its dependence on the parameter valuation 𝜔 is strongly measurable: for every u ∈ H𝑞, the map 𝜔 ↦→ 𝑈𝜔u is measurable; for a while command, it is admissible if the two-outcome loop guard {𝑀𝜔,0, 𝑀𝜔,1} satisfying the same strongl… view at source ↗
Figure 2
Figure 2. Figure 2: Proof system for validity 5.3 Proof System We present in [PITH_FULL_IMAGE:figures/full_fig_p017_2.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

112 extracted references · 10 canonical work pages

  1. [1]

    2006.Infinite dimensional analysis: a hitchhiker’s guide

    Charalambos D Aliprantis and Kim C Border. 2006.Infinite dimensional analysis: a hitchhiker’s guide. Springer Berlin, Heidelberg, Heidelberg

    2006

  2. [2]

    Andris Ambainis, Eric Bach, Ashwin Nayak, Ashvin Vishwanath, and John Watrous. 2001. One-Dimensional Quantum Walks. InProceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing. ACM, Hersonissos Greece, 26 Tianshi Yu, Gilles Barthe, Minbo Gao, Mingsheng Ying, and Li Zhou 37–49. doi:10.1145/380752.380757

    arXiv 2001

  3. [3]

    Warit Asavanant, Yu Shiozawa, Shota Yokoyama, Baramee Charoensombutamon, Hiroki Emura, Rafael N Alexander, Shuntaro Takeda, Jun-ichi Yoshikawa, Nicolas C Menicucci, Hidehiro Yonezawa, et al . 2019. Generation of time- domain-multiplexed two-dimensional cluster state.Science366, 6463 (2019), 373–376

    2019

  4. [4]

    Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix, and Vladimir Zamdzhiev. 2022. Quantum expectation transformers for cost analysis. InProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. 1–13

    2022

  5. [5]

    Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan, Matthijs Muis, Ivan Renison, Keiya Sakabe, Michael Walter, Yingte Xu, Tianshi Yu, and Li Zhou. 2026. Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions. In41st Annual Symposium on Logic in Computer Science (LICS 2026) (Leibniz International Proceedings in Informatics...

    2026

  6. [6]

    Gilles Barthe, Minbo Gao, Theo Wang, and Li Zhou. 2025. Complete Quantum Relational Hoare Logics from Optimal Transport Duality. In2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 884–925. doi:10. 1109/LICS65433.2025.00072

    arXiv 2025

  7. [7]

    Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2021. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning.Proceedings of the ACM on Programming Languages5, POPL (2021), 1–30

    2021

  8. [8]

    2020.Boundary value problems, Weyl functions, and differential operators

    Jussi Behrndt, Seppo Hassi, and Henk De Snoo. 2020.Boundary value problems, Weyl functions, and differential operators. Springer Nature

    2020

  9. [9]

    Jussi Behrndt, Seppo Hassi, Henk de Snoo, and Rudi Wietsma. 2010. Monotone convergence theorems for semi-bounded operators and forms with applications.Proceedings of the Royal Society of Edinburgh: Section A Mathematics140, 5 (2010), 927–951. doi:10.1017/S030821050900078X

    work page doi:10.1017/s030821050900078x 2010

  10. [10]

    Eli Bourassa, Rafael N

    J. Eli Bourassa, Rafael N. Alexander, Michael Vasmer, Ashlesha Patil, Ilan Tzitrin, Takaya Matsuura, Daiqin Su, Ben Q. Baragiola, Saikat Guha, Guillaume Dauphinais, Krishna K. Sabapathy, Nicolas C. Menicucci, and Ish Dhand. 2021. Blueprint for a Scalable Photonic Fault-Tolerant Quantum Computer.Quantum5 (Feb. 2021), 392. doi:10.22331/q- 2021-02-04-392

    doi:10.22331/q- 2021

  11. [11]

    Samuel L Braunstein and Peter Van Loock. 2005. Quantum information with continuous variables.Reviews of modern physics77, 2 (2005), 513–577

    2005

  12. [12]

    Philippe Campagne-Ibarcq, Alec Eickbusch, Steven Touzard, Evan Zalys-Geller, Nicholas E Frattini, Volodymyr V Sivak, Philip Reinhold, Shruti Puri, Shyam Shankar, Robert J Schoelkopf, et al. 2020. Quantum error correction of a qubit encoded in grid states of an oscillator.Nature584, 7821 (2020), 368–372

    2020

  13. [13]

    Kean Chen, Yuhao Liu, Wang Fang, Jennifer Paykin, Xin-Chuan Wu, Albert Schmitz, Steve Zdancewic, and Gushu Li

  14. [14]

    Youngchan Cho and Robert Rand. 2026. Efficiently Verifying Quantum Programs with Few T Gates. InVerification, Model Checking, and Abstract Interpretation, Yu-Fang Chen, Thomas Jensen, and Ondvrej Lengál (Eds.). Springer Nature Switzerland, Cham, 44–57

    2026

  15. [15]

    Donald L. Cohn. 2013.Measure Theory(2 ed.). Birkhäuser, New York. doi:10.1007/978-1-4614-6956-8

    doi:10.1007/978-1-4614-6956-8 2013

  16. [16]

    1998.Multivalued linear operators

    Ronald Cross. 1998.Multivalued linear operators. Vol. 213. CRC Press

    1998

  17. [17]

    Edward Brian Davies. 1976. Quantum theory of open systems. (1976)

    1976

  18. [18]

    Ellie D’Hondt and Prakash Panangaden. 2006. Quantum weakest preconditions.Mathematical Structures in Computer Science16, 3 (2006), 429–451. doi:10.1017/S0960129506005251

    doi:10.1017/s0960129506005251 2006

  19. [19]

    Diestel and J

    J. Diestel and J. J. Uhl. 1977.Vector Measures. Mathematical Surveys and Monographs, Vol. 15. American Mathematical Society

    1977

  20. [20]

    Dunford and J.T

    N. Dunford and J.T. Schwartz. 1988.Linear Operators, Part 1: General Theory. Wiley, New York, NY, USA

    1988

  21. [21]

    Mattias Ehatamm, Yi Lee, Xiaodi Wu, and Runzhou Tao. 2026. End-to-End Formalization of Quantum Error Correction. arXiv:2605.16523 [quant-ph]

    Pith/arXiv arXiv 2026

  22. [22]

    Wang Fang and Mingsheng Ying. 2024. Symbolic Execution for Quantum Error Correction Programs.Proc. ACM Program. Lang.8, PLDI, Article 189 (June 2024), 26 pages. doi:10.1145/3656419

    doi:10.1145/3656419 2024

  23. [23]

    Yuan Feng and Mingsheng Ying. 2021. Quantum Hoare Logic with Classical Variables.ACM Transactions on Quantum Computing2, 4, Article 16 (Dec. 2021), 43 pages. doi:10.1145/3456877

    doi:10.1145/3456877 2021

  24. [24]

    Christa Flühmann, Thanh Long Nguyen, Matteo Marinelli, Vlad Negnevitsky, Karan Mehta, and JP Home. 2019. Encoding a qubit in a trapped-ion mechanical oscillator.Nature566, 7745 (2019), 513–517

    2019

  25. [25]

    Christina Gehnen, Dominique Unruh, and Joost-Pieter Katoen. 2025. Bayesian Inference in Quantum Programs. In52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 334), Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, and Gabriele Puppis (Eds.). Schloss Reas...

    doi:10.4230/lipi 2025

  26. [26]

    Daniel Gottesman, Alexei Kitaev, and John Preskill. 2001. Encoding a qubit in an oscillator.Physical Review A64, 1 (2001), 012310

    2001

  27. [27]

    2001.Statistical structure of quantum theory

    Alexander S Holevo. 2001.Statistical structure of quantum theory. Springer Science & Business Media

    2001

  28. [28]

    2011.Probabilistic and statistical aspects of quantum theory

    Alexander S Holevo. 2011.Probabilistic and statistical aspects of quantum theory. Vol. 1. Springer Science & Business Media, Berlin, Heidelberg

    2011

  29. [29]

    Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, and Mingsheng Ying. 2025. Efficient Formal Verification of Quantum Error Correcting Programs.Proc. ACM Program. Lang.9, PLDI, Article 190 (June 2025), 26 pages. doi:10.1145/3729293

    doi:10.1145/3729293 2025

  30. [30]

    2016.Analysis in Banach spaces

    Tuomas Hytönen, Jan Van Neerven, Mark Veraar, and Lutz Weis. 2016.Analysis in Banach spaces. Vol. 1. Springer

    2016

  31. [31]

    1997.Fundamentals of the Theory of Operator Algebras

    Richard V Kadison and John R Ringrose. 1997.Fundamentals of the Theory of Operator Algebras. Vol. 2. American Mathematical Soc

    1997

  32. [32]

    Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2018. Weakest precondition reasoning for expected runtimes of randomized algorithms.Journal of the ACM (JACM)65, 5 (2018), 1–68

    2018

  33. [33]

    2013.Perturbation theory for linear operators

    Tosio Kato. 2013.Perturbation theory for linear operators. Vol. 132. Springer Science & Business Media

    2013

  34. [34]

    J Kempe. 2003. Quantum random walks: An introductory overview.Contemporary Physics44, 4 (2003), 307–327. doi:10.1080/00107151031000110776

    doi:10.1080/00107151031000110776 2003

  35. [35]

    Dexter Kozen. 1981. Semantics of probabilistic programs.J. Comput. System Sci.22, 3 (1981), 328–350. doi:10.1016/0022- 0000(81)90036-2

    doi:10.1016/0022- 1981

  36. [36]

    Karl Kraus. 1971. General state changes in quantum theory.Annals of Physics64, 2 (1971), 311–335

    1971

  37. [37]

    Zaki Leghtas, Gerhard Kirchmair, Brian Vlastakis, Robert J Schoelkopf, Michel H Devoret, and Mazyar Mirrahimi

  38. [38]

    Yangjia Li and Dominique Unruh. 2021. Quantum Relational Hoare Logic with Expectations. In48th International Colloquium on Automata, Languages, and Programming (ICALP 2021) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 198), Nikhil Bansal, Emanuela Merelli, and James Worrell (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dag...

    work page doi:10.4230/lipics.icalp.2021.136 2021

  39. [39]

    Yangjia Li and Mingsheng Ying. 2018. Algorithmic Analysis of Termination Problems for Quantum Programs. Proceedings of the ACM on Programming Languages2, POPL, Article 35 (2018), 35:1–35:29 pages. doi:10.1145/3158123

    work page doi:10.1145/3158123 2018

  40. [40]

    Junyi Liu, Li Zhou, Gilles Barthe, and Mingsheng Ying. 2025. Quantum weakest preconditions for reasoning about expected runtimes of quantum programs.J. ACM72, 3 (2025), 1–51

    2025

  41. [41]

    Braunstein

    Seth Lloyd and Samuel L. Braunstein. 1999. Quantum Computation over Continuous Variables.Physical Review Letters 82, 8 (Feb. 1999), 1784–1787. doi:10.1103/PhysRevLett.82.1784

    doi:10.1103/physrevlett.82.1784 1999

  42. [42]

    Lars S Madsen, Fabian Laudenbach, Mohsen Falamarzi Askarani, Fabien Rortais, Trevor Vincent, Jacob FF Bulmer, Filippo M Miatto, Leonhard Neuhaus, Lukas G Helt, Matthew J Collins, et al. 2022. Quantum computational advantage with a programmable photonic processor.Nature606, 7912 (2022), 75–81

    2022

  43. [43]

    Takaya Matsuura, Hayata Yamasaki, and Masato Koashi. 2020. Equivalence of approximate Gottesman-Kitaev-Preskill codes.Physical Review A102, 3 (2020), 032408

    2020

  44. [44]

    2005.Abstraction, Refinement and Proof for Probabilistic Systems

    Annabelle McIver and Carroll Morgan. 2005.Abstraction, Refinement and Proof for Probabilistic Systems. Springer. doi:10.1007/B138392

    doi:10.1007/b138392 2005

  45. [45]

    Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers.ACM Transactions on Programming Languages and Systems18, 3 (May 1996), 325–353. doi:10.1145/229542.229547

    arXiv 1996

  46. [46]

    Masanao Ozawa. 1984. Quantum measuring processes of continuous observables.J. Math. Phys.25, 1 (1984), 79–87

    1984

  47. [47]

    Robert Rand, Aarthi Sundaram, Kartik Singhal, and Brad Lackey. 2021. Gottesman Types for Quantum Programs. Electronic Proceedings in Theoretical Computer Science340 (Sept. 2021), 279–290. doi:10.4204/eptcs.340.14

    work page doi:10.4204/eptcs.340.14 2021

  48. [48]

    1980.Methods of modern mathematical physics: Functional analysis

    Michael Reed and Barry Simon. 1980.Methods of modern mathematical physics: Functional analysis. Vol. 1. Gulf Professional Publishing

    1980

  49. [49]

    1987.Real and complex analysis

    Walter Rudin. 1987.Real and complex analysis. McGraw-Hill, Inc

    1987

  50. [50]

    2012.Unbounded self-adjoint operators on Hilbert space

    Konrad Schmüdgen. 2012.Unbounded self-adjoint operators on Hilbert space. Vol. 265. Springer Science & Business Media

    2012

  51. [51]

    Peter Selinger. 2004. Towards a quantum programming language.Mathematical Structures in Computer Science14, 4 (2004), 527–586

    2004

  52. [52]

    Barry Simon. 1978. Lower semicontinuhy of positive quadratic forms.Proceedings of the Royal Society of Edinburgh: Section A Mathematics79, 3–4 (1978), 267–273. doi:10.1017/S0308210500019776

    work page doi:10.1017/s0308210500019776 1978

  53. [53]

    Aarthi Sundaram, Robert Rand, Kartik Singhal, Youngchan Cho, and Brad Lackey. 2026. Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs. arXiv:2101.08939 [quant-ph]

    Pith/arXiv arXiv 2026

  54. [54]

    Barbara M Terhal, Jonathan Conrad, and Christophe Vuillot. 2020. Towards scalable bosonic quantum error correction. Quantum Science and Technology5, 4 (2020), 043001. 28 Tianshi Yu, Gilles Barthe, Minbo Gao, Mingsheng Ying, and Li Zhou

    2020

  55. [55]

    Tse, Haocun Yu, N

    M. Tse, Haocun Yu, N. Kijbunchoo, A. Fernandez-Galiana, P. Dupej, L. Barsotti, C. D. Blair, D. D. Brown, S. E. Dwyer, A. Effler, M. Evans, P. Fritschel, V. V. Frolov, A. C. Green, G. L. Mansell, F. Matichard, N. Mavalvala, D. E. McClelland, L. McCuller, T. McRae, J. Miller, A. Mullavey, E. Oelker, I. Y. Phinney, D. Sigg, B. J. J. Slagmolen, T. Vo, R. L. W...

    2019

  56. [56]

    Dominique Unruh. 2019. Quantum Hoare Logic with Ghost Variables. In2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1–13. doi:10.1109/LICS.2019.8785779

    arXiv 2019

  57. [57]

    Dominique Unruh. 2019. Quantum Relational Hoare Logic.Proc. ACM Program. Lang.3, POPL, Article 33 (Jan. 2019), 31 pages. doi:10.1145/3290346

    doi:10.1145/3290346 2019

  58. [58]

    Dominique Unruh. 2024. Quantum references. arXiv:2105.10914 [cs.LO]

    Pith/arXiv arXiv 2024

  59. [59]

    Henning Vahlbruch, Moritz Mehmet, Karsten Danzmann, and Roman Schnabel. 2016. Detection of 15 dB squeezed states of light and their application for the absolute calibration of photoelectric quantum efficiency.Physical review letters117, 11 (2016), 110801

    2016

  60. [60]

    Christian Weedbrook, Stefano Pirandola, Raúl García-Patrón, Nicolas J Cerf, Timothy C Ralph, Jeffrey H Shapiro, and Seth Lloyd. 2012. Gaussian quantum information.Reviews of modern physics84, 2 (2012), 621–669

    2012

  61. [61]

    Michael M. Wolf. 2023. Mathematical Introduction to Quantum Information Processing. Lecture notes, Technical University of Munich. https://mediatum.ub.tum.de/doc/1706981/document.pdf Growing lecture notes, 2019/2022, version Mar. 2023

    arXiv 2023

  62. [62]

    Anbang Wu, Gushu Li, Hezi Zhang, Gian Giacomo Guerreschi, Yuan Xie, and Yufei Ding. 2021. QECV: Quantum Error Correction Verification. arXiv:2111.13728 [quant-ph]

    Pith/arXiv arXiv 2021

  63. [63]

    Mingsheng Ying. 2011. Floyd–hoare logic for quantum programs.ACM Transactions on Programming Languages and Systems (TOPLAS)33, 6, Article 19 (2011), 49 pages. doi:10.1145/2049706.2049708

    arXiv 2011

  64. [64]

    Mingsheng Ying. 2019. Toward Automatic Verification of Quantum Programs.Formal Aspects of Computing31, 1 (2019), 3–25. doi:10.1007/s00165-018-0465-3

    work page doi:10.1007/s00165-018-0465-3 2019

  65. [65]

    Mingsheng Ying. 2022. Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs. arXiv:2205.01959 [cs.LO] doi:10.48550/arXiv.2205.01959

    Pith/arXiv arXiv doi:10.48550/arxiv.2205.01959 2022

  66. [66]

    Mingsheng Ying, Runyao Duan, Yuan Feng, and Zhengfeng Ji. 2010. Predicate Transformer Semantics of Quantum Programs. InSemantic Techniques in Quantum Computation, Simon J. Gay and Ian Mackie (Eds.). Cambridge University Press, 311–360. doi:10.1017/CBO9781139193313.009

    work page doi:10.1017/cbo9781139193313.009 2010

  67. [67]

    Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. 2017. Invariants of Quantum Programs: Characterisations and Generation. InProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). Association for Computing Machinery, 818–832. doi:10.1145/3009837.3009840

    arXiv 2017

  68. [68]

    Mingsheng Ying, Nengkun Yu, Yuan Feng, and Runyao Duan. 2013. Verification of Quantum Programs.Science of Computer Programming78, 9 (2013), 1679–1700. doi:10.1016/j.scico.2013.03.016

    work page doi:10.1016/j.scico.2013.03.016 2013

  69. [69]

    Mingsheng Ying, Li Zhou, and Gilles Barthe. 2026. Laws of Quantum Programming.ACM Trans. Softw. Eng. Methodol. 35, 7, Article 191 (June 2026), 37 pages. doi:10.1145/3765903

    work page doi:10.1145/3765903 2026

  70. [70]

    Mingsheng Ying, Li Zhou, and Yangjia Li. 2018. Reasoning about Parallel Quantum Programs. arXiv:1810.11334 [cs.LO]

    Pith/arXiv arXiv 2018

  71. [71]

    Nengkun Yu. 2023. Structured Theorem for Quantum Programs and Its Applications.ACM Transactions on Software Engineering and Methodology32, 4, Article 103 (2023). doi:10.1145/3587154 Reasoning about Continuous-Variable Quantum Systems 29

    work page doi:10.1145/3587154 2023

  72. [72]

    Li Zhou, Nengkun Yu, and Mingsheng Ying. 2019. An applied quantum Hoare logic. InProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM, 1149–1162. doi:10.1145/3314221.3314584 The Guide of Appendices The appendices ...

    arXiv 2019

  73. [75]

    By the definition of closure, the domain Dom(𝑇) is dense inDom(𝔱 𝑇)with respect to the form norm

    From Relation to Form (𝑇↦→𝔱 𝑇 ):Given a positive self-adjoint linear relation𝑇, we define 𝔱𝑇 as the closure of the minimal form 𝔱0[u]=⟨ w, u⟩ for any(u, w) ∈𝑇 andv ∈Dom(𝑇) , as constructed in Definition A.5 and Definition A.6. By the definition of closure, the domain Dom(𝑇) is dense inDom(𝔱 𝑇)with respect to the form norm

  74. [76]

    continue

    Bijectivity (Inverse Property):Starting from 𝔱 and then forming the minimal form of𝑇𝔱 gives the restriction of 𝔱 to Dom(𝐴)=Ran(𝐵) . By Lemma A.1, Ran(𝐵) is dense in Dom(𝔱) in the form norm; hence the closure is exactly𝔱. Starting from𝑇 , take(u, w)∈𝑇 . Forv ∈Dom(𝔱 𝑇), choosev 𝑛∈Dom(𝑇) withv𝑛→ vin the form norm. Then 𝔱𝑇[u,v]=lim 𝑛 𝔱0[u,v𝑛]=lim 𝑛 ⟨w,v𝑛⟩H =⟨...

  75. [77]

    We show that Í 𝑖 𝔱𝑄[𝐾𝑖 u]= Í 𝑗 𝔱𝑄[𝐿𝑗 u]for any𝑢∈H

    Independence.Let {𝐾𝑖} and{𝐿𝑗} be two countable Kraus representations of J𝑆K. We show that Í 𝑖 𝔱𝑄[𝐾𝑖 u]= Í 𝑗 𝔱𝑄[𝐿𝑗 u]for any𝑢∈H. We invoke Proposition A.4 (Spectral Approximation). There exists a sequence ofboundedpred- icates{𝑄𝑛}𝑛∈N such that𝑄𝑛⊑𝑄 𝑛+1 and 𝔱𝑄[v]=sup 𝑛 𝔱𝑄𝑛[v] for allv. Let 𝐴𝑛∈B(H) be the bounded operator associated with each𝑄 𝑛 (i.e.,𝔱𝑄𝑛[v]=...

  76. [78]

    By the spectral approximation𝑄= Ã 𝑛𝑄𝑛 used above, and the continuity of the trace over positive forms, we have: Tr(𝑄J𝑆K(𝜌))=sup 𝑛 Tr 𝑄𝑛J𝑆K(𝜌)

    Exact Duality.Let 𝜌∈D(H) have the spectral decomposition𝜌= Í 𝑘𝜆𝑘 Pu𝑘 . By the spectral approximation𝑄= Ã 𝑛𝑄𝑛 used above, and the continuity of the trace over positive forms, we have: Tr(𝑄J𝑆K(𝜌))=sup 𝑛 Tr 𝑄𝑛J𝑆K(𝜌) . For the bounded operator𝑄 𝑛, the trace evaluates standardly: Tr 𝑄𝑛J𝑆K(𝜌) = ∑︁ 𝑘 𝜆𝑘 Tr 𝑄𝑛J𝑆K(P u𝑘) = ∑︁ 𝑘 𝜆𝑘 ∑︁ 𝑖 𝔱𝑄𝑛[𝐾𝑖 u𝑘]. Reasoning about C...

  77. [79]

    • Validity:By the Exact Duality established above,Tr(wlp(𝑆,𝑄)𝜌)=Tr(𝑄J𝑆K(𝜌))≥Tr(𝑄J𝑆K(𝜌))

    Semantic Minimality and Uniqueness.We now prove that the constructed form satisfies both conditions of Definition C.3. • Validity:By the Exact Duality established above,Tr(wlp(𝑆,𝑄)𝜌)=Tr(𝑄J𝑆K(𝜌))≥Tr(𝑄J𝑆K(𝜌)) . The inequality is trivially satisfied, ensuring|=𝑝𝑎𝑟{wlp(𝑆,𝑄)}𝑆{𝑄}. • Minimality:Suppose 𝑃∈P is any valid precondition such that|=𝑝𝑎𝑟{𝑃}𝑆{𝑄} . By va...

  78. [80]

    By definition, Dom(𝔱𝑄)⊆Dom(𝔱 𝑃) and 𝔱𝑃[v]≤𝔱 𝑄[v] for all v∈Dom(𝔱 𝑄)

    Monotonicity.Let 𝑃⊑𝑄 . By definition, Dom(𝔱𝑄)⊆Dom(𝔱 𝑃) and 𝔱𝑃[v]≤𝔱 𝑄[v] for all v∈Dom(𝔱 𝑄). For the domain, ifu∈Dom(𝔱 wlp(𝑆,𝑄)), then𝐾𝑖 u∈Dom(𝔱 𝑄)⊆Dom(𝔱 𝑃) for all𝑖, and the sum converges. Thus Dom(𝔱wlp(𝑆,𝑄))⊆Dom(𝔱 wlp(𝑆,𝑃)). For the value, since 𝔱𝑃[𝐾𝑖 u]≤𝔱 𝑄[𝐾𝑖 u], summing over𝑖preserves the inequality

  79. [81]

    By Theorem A.3, the form 𝔱𝑃 is defined by 𝔱𝑃[v]=Í 𝑗𝑐𝑗 𝔱𝑃 𝑗[v]and is a closed form

    Countable Additivity.Let 𝑃= Í 𝑗𝑐𝑗𝑃𝑗. By Theorem A.3, the form 𝔱𝑃 is defined by 𝔱𝑃[v]=Í 𝑗𝑐𝑗 𝔱𝑃 𝑗[v]and is a closed form. Then for anyu: 𝔱wlp(𝑆,𝑃)[u]= ∑︁ 𝑖 𝔱𝑃[𝐾𝑖 u] = ∑︁ 𝑖 ∑︁ 𝑗 𝑐𝑗 𝔱𝑃 𝑗[𝐾𝑖 u] ! . Since all terms𝑐𝑗 𝔱𝑃 𝑗[𝐾𝑖 u] are non-negative, by Tonelli’s theorem for series (infinite associativity and commutativity of non-negative sums, [49]), we can exchang...

  80. [82]

    By Theo- rem A.3,𝔱𝑃(v)=sup 𝑛 𝔱𝑃𝑛(v)

    Scott-Continuity.Let 𝑃𝑛 be an increasing sequence with supremum𝑃= Ã 𝑛𝑃𝑛. By Theo- rem A.3,𝔱𝑃(v)=sup 𝑛 𝔱𝑃𝑛(v). Then: 𝔱wlp(𝑆,𝑃)[u]= ∑︁ 𝑖 sup 𝑛 𝔱𝑃𝑛[𝐾𝑖 u]. Since the sequence{𝔱𝑃𝑛(𝐾𝑖 u)}𝑛 is non-decreasing for each𝑖, we can apply the Monotone Conver- gence Theorem for series (interchanging sum and supremum):∑︁ 𝑖 sup 𝑛 𝔱𝑃𝑛[𝐾𝑖 u]=sup 𝑛 ∑︁ 𝑖 𝔱𝑃𝑛[𝐾𝑖 u]=sup 𝑛 𝔱wlp(...

Showing first 80 references.