Pith. sign in

REVIEW 3 major objections 5 minor 58 references

First Hoare logic verifies continuous-variable quantum programs

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 17:12 UTC pith:OYPBGHF2

load-bearing objection First unary Hoare logic for continuous-variable quantum programs, with an elegant syntactic substitution calculus and a real but fixable gap in the trace-interchange argument. the 3 major comments →

arxiv 2607.17714 v1 pith:OYPBGHF2 submitted 2026-07-20 quant-ph cs.LO

Formal Verification of Continuous-Variable Quantum Programs

Stefanie Muroya , Thomas A. Henzinger This is my paper
classification quant-ph cs.LO MSC 68Q6081P68 PACS 03.67.Lx03.65.-w
keywords continuous-variable quantum computingHoare logicweakest preconditionprogram verificationSchwartz density operatorspolynomial observablesFock measurementresource estimation
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 tries to establish the first unary Hoare logic for continuous-variable quantum computing (CQC), where programs act on infinite-dimensional Hilbert spaces and measurement outcomes can be unbounded. The central claim is that a proof system whose assertions are polynomial inequalities over the canonical position and momentum observables is sound and relatively complete, provided states are restricted to physically realistic Schwartz density operators and programs are loop-free. If the logic is right, photonic quantum programs can be verified deductively rather than by simulation, and the same weakest-precondition calculus yields quantitative guarantees: finite-squeezing noise, homodyne estimation error, equivalence of gate decompositions, and rigorous bounds on Fock-state truncation for classical simulation. The paper backs the claim with a formal denotational and dual semantics, closure theorems, a symbolic weakest-precondition implementation, and textbook case studies.

Core claim

On the paper's own terms, the discovery is that the three things separating continuous-variable quantum programming from discrete-variable programming—infinite-dimensional Hilbert space, unbounded observables, and possibly divergent expectation values—can be contained by three coordinated choices: restrict the state space to Schwartz density operators; build assertions from finite polynomials over the quadrature and ladder operators; and interpret each assertion as a set of density operators rather than as an observable in the Löwner order. The authors then define the programming language CvQPL, prove that Schwartz density operators are invariant under every instruction, prove that polynomia

What carries the argument

The load-bearing machinery is the assertion language A: finite polynomials over the canonical observables X_q, P_q, A_q, A_q†, read as inequalities between expectation values, with each assertion denoting a set of Schwartz density operators. Around it, three pieces do the work: the Schwartz-space restriction (which makes every polynomial expectation finite and is closed under all program instructions); the dual semantics of CvQPL, computed by syntactic substitution rather than operator manipulation; and the duality theorem Corollary 2, which lets the weakest-precondition transformer play the Heisenberg picture against the forward Schrödinger semantics. Fock-basis closure lemmas for measureme

Load-bearing premise

The proof of the duality theorem for Fock measurements assumes that the infinite sum over measurement outcomes commutes with taking the trace of an unbounded polynomial observable; if this interchange fails, the weakest-precondition transformer and the Atom rule would not be sound.

What would settle it

Evaluate both sides of Corollary 2 for a concrete instance, e.g. the vacuum or a squeezed state, with Z = X^4 under Meas(q): compute the infinite sum Σ_i Tr(Z Λ_i ρ Λ_i) termwise and compare it with Tr(Z Σ_i Λ_i ρ Λ_i) obtained by the polynomial substitution. A mismatch would refute the duality theorem; an explicit dominated-convergence proof for the estimate |Tr(JMeasK*(Z)ρ)| < ∞ would confirm the step.

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

If this is right

  • Continuous-variable programs can be verified deductively: the tool derives weakest preconditions that certify homodyne measurement, Deutsch-Jozsa/Bernstein-Vazirani, superdense coding, and teleportation against their specifications.
  • The same calculus extracts quantitative noise formulas: finite-squeezing variances and single-shot measurement noise emerge from quadratic postconditions, giving explicit parameter-selection criteria for hardware.
  • Unitary equivalence of continuous-variable circuits, up to global phase, reduces to comparing weakest preconditions on the two quadratures X and P, which the authors use to check gate decompositions.
  • Classical simulation gets rigorous error bounds: weakest preconditions for the number operator, combined with a one-sided Chebyshev-Cantelli inequality, tell how many Fock states must be kept for a target accuracy.
  • With such truncation bounds, the infinite-dimensional space becomes effectively finite, so discrete-variable verification tools can be reused for continuous-variable programs with soundness guarantees.

Where Pith is reading between the lines

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

  • The loop-free restriction is the next pressure point: extending the logic to while-like programs would need a fixed-point principle over polynomial assertions, and it is unclear that syntactic substitution survives iteration.
  • The relative-completeness oracle decides entailment of polynomial inequalities over Schwartz density operators; in practice that is a real-algebraic decision problem, so the automation's cost will be dominated by quantifier elimination or polynomial-solving rather than by the quantum structure.
  • The same set-based semantics could in principle migrate to other settings with unbounded observables, such as quantum field theories or infinite lattice models, whenever a dense stable domain analogous to the Schwartz space exists.
  • A testable extension is to add selective measurements and classical feed-forward; the current non-selective semantics matches today's straight-line hardware but excludes measurement-based protocols, where the duality theorem would need re-examination.

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

3 major / 5 minor

Summary. The paper introduces CvQPL, a straight-line continuous-variable quantum programming language with Fock-basis measurements, vacuum resets, and standard Gaussian and non-Gaussian gates, together with CvQHL, a unary Hoare logic whose assertions are Boolean combinations of polynomial inequalities over canonical quadrature and ladder operators. The authors restrict the semantic state space to Schwartz density operators P, use set-based entailment on P, and compute weakest preconditions by syntactic substitution. They prove soundness and relative completeness of the proof system, and report a Python/SymPy tool that derives weakest preconditions for textbook algorithms, verifies gate decompositions, and estimates Fock-truncation resources for classical simulation.

Significance. If the technical gaps in the trace arguments are repaired, this is a substantial contribution: it provides the first unary Hoare logic for continuous-variable quantum programs, directly addressing the infinite-dimensional and unbounded-observable obstacles that block naive extension of DQC logics. The choice of Schwartz density operators is principled, the polynomial assertion language is natural and readable, and the syntactic-substitution weakest-precondition transformer is a genuine algorithmic advance over semantic infinite-dimensional manipulations. The paper ships a working symbolic tool and derives concrete, falsifiable quantitative predictions (e.g., 1/r^2 homodyne noise and e^{-2r}/2 finite-squeezing variance). The central soundness claim, however, currently rests on unproved trace/infinite-sum interchanges for unbounded observables.

major comments (3)
  1. [Theorem 1, Measurements bullet] The finite-trace part asserts the chain |Tr(Z JMeasK*(Z)ρ)| = |Tr(Z Λ0ρΛ0) + Tr(Z Λ1ρΛ1) + ...| = |Tr(Z Σ_i Λ_i ρ Λ_i)|. Termwise cyclicity only justifies equality for each finite partial sum, since each Λ_i is bounded. Moving the infinite sum inside the trace of the unbounded polynomial Z requires a dominated-convergence or trace-norm argument, which is not supplied. Proposition 5(2) gives super-polynomial decay of the Fock entries of ρ and the diagonal entries of Z grow at most polynomially, so an absolute-convergence argument is available, but it is absent. This gap is load-bearing: Corollary 2, Lemma 6, and the Atom rule in Figure 7 all rely on the resulting duality identity. The same issue appears in the Reset bullet, where the finite-trace proof is only described as 'analogous'.
  2. [Theorem 1, Atomic unitaries bullet] The proof asserts that U†ZUρ is trace class because U†ZU is again a polynomial. This does not follow: the product of an unbounded polynomial observable with a trace-class operator need not be trace class, and the subsequent manipulations with √ρ and the cyclic property require that trace-class status. The paper needs a systematic lemma establishing that for Z∈Ξ_f^† and ρ∈P, products such as Zρ, U†ZU ρ, and the related operator products are trace class, using the Schwartz decay of ρ's matrix elements. Without such a lemma, the atomic-unitary part of Theorem 1, and hence the invariance of P, is not fully proved.
  3. [Corollary 2] Corollary 2 is stated as an immediate consequence of Theorem 1, but Theorem 1 establishes only finiteness of expectations, not the duality equality Tr(JMeasK*(Z)ρ)=Tr(Z JMeasK(ρ)) for all ρ∈P and all polynomial Z. In the measurement case the equality is exactly the unproved interchange identified above. Since Corollary 2 is used in Lemma 6 to prove exactness of SubA, and Lemma 6 underpins the soundness of the Atom rule and the weakest-precondition characterization, the soundness and relative-completeness theorems are conditional on this repair. A short dominated-convergence lemma using the decay estimate from Proposition 5(2) would close the gap.
minor comments (5)
  1. [Figure 1] The syntax entries D(q,r,r) and BS(q0,q1,r,r) use the same symbol r for both parameters, while the semantics in Figure 2 uses r0 and r1. Standardize the notation.
  2. [Example 1] The displayed formula for α(x) is missing parentheses: it should read α(x)=1/(√2(1+|x|)), and the integrand should be x/(2(1+|x|)^2). As typeset, the equation is hard to parse.
  3. [Example 2] The heading says 'under sqeeze'; typo for 'squeezing'. Equation (1) is also poorly typeset, with missing parentheses and an unclear integrand; since the paper intentionally says the reader need not understand it, consider trimming or reformatting.
  4. [Figure 10] The precondition contains the tautological conjuncts (x=x)∧(p=p) and overloads x and p as both symbolic message values and expectation variables. This makes the triple harder to read; clarify the naming convention.
  5. [Figure 9(b)] The weakest-precondition terms, e.g., 'X_q0 + sqrt2 X_q2 / e^r = x', have ambiguous operator precedence. Parentheses around the numerator and denominator would help.

Circularity Check

0 steps flagged

No circularity found: CvQHL's weakest-precondition calculus is derived from stated semantics and external mathematics, not from its conclusions.

full rationale

We find no circular step in the paper's central derivation. CvQHL's assertion semantics (Figure 5), the dual semantics of CvQPL (Figures 2 and 3), and the syntactic substitution transformer (Equations 8-10) are defined directly; Lemmas 4-6 and Corollaries 1-4 establish by structural induction that SubA computes the semantic weakest precondition, with the duality Corollary 2 resting on Theorem 1. The case-study quantities (e.g., the 1/r^2 homodyne noise, the e^{-2r}/2 squeezing variance, and the number-operator weakest preconditions in Figure 11) are symbolic outputs of this transformer, not fitted parameters, and the paper explicitly presents them as recovered textbook results. The equivalence checking uses externally proved Stone-von Neumann/Schur's lemma results (Proposition 6), and the only closely related prior work [4] is a different relational logic, not a self-citation. The one substantive concern, an unproved interchange of an infinite Fock-basis sum with the trace of an unbounded polynomial in Theorem 1's measurement case, would be a soundness gap if unfixable; it is not a reduction of the claimed result to its own inputs, so it does not affect the circularity score.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 0 invented entities

The central claim rests on restricting to Schwartz density operators, closure of that class under the instruction semantics, standard harmonic-analysis facts, and a partial assertion semantics. There are no fitted parameters and no new physical entities.

axioms (6)
  • domain assumption The physically relevant state space is exactly the set of Schwartz density operators P.
    Section 1.1 and Section 2.0.1: the logic applies only to states with Schwartz decay so all polynomial expectations are finite. If useful physical states lie outside P, the logic does not cover them.
  • standard math Gaussian unitaries preserve the Schwartz space.
    Lemma 3 proof cites [19,22,24]; needed to prove closure of P under D, S, R, and BS instructions.
  • standard math Canonical observables form an irreducible set; unitaries agreeing on them differ by a global phase.
    Proposition 6 relies on the Stone-von Neumann theorem and Schur's lemma; used for gate-equivalence checking.
  • domain assumption Assertion comparisons are interpreted only when both quantum terms are self-adjoint, and any polynomial can be symmetrized.
    Section 4.1 remark: the syntax admits non-self-adjoint ladder terms A_q and A_q^dagger, making the semantic interpretation partial unless comparisons are restricted or symmetrized.
  • domain assumption The programming language is loop-free and terminating.
    Section 1.3: only straight-line programs are considered, matching current quantum hardware which has no native loops or conditionals.
  • domain assumption Natural units with ℏ = m = 1 and ω = 1.
    Section 2 remark: simplifies algebra without altering soundness, but ties numerical interpretations to this normalization.

pith-pipeline@v1.3.0-alltime-deepseek · 32207 in / 18656 out tokens · 198655 ms · 2026-08-01T17:12:13.585517+00:00 · methodology

0 comments
read the original abstract

We provide a formal framework for Continuous-Variable Quantum Computing (CQC). While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for continuous-variable quantum programs nor of a unary Hoare logic for their verification. There are several technical obstacles to extending to CQC any of the formal frameworks available for Discrete-Variable Quantum Computing (DQC). Most importantly, continuous-variable quantum programs act on {\em infinite-dimensional} Hilbert spaces; their measurement outcomes are often {\em unbounded} and have expected values that are defined by an improper integral (or an infinite series), which may not converge. We overcome these challenges to give a formal semantics to a universal programming language for CQC and to provide the first Hoare logic for CQC. The assertions of our logic are built from polynomials over canonical observables. Besides proving relative completeness, we implement a symbolic weakest-precondition calculator for CQC based on our logic. Our tool has successfully verified CQC algorithms from textbooks and calculated their approximation errors for physically realizable implementations, proved the correctness (i.e., equivalence) of gate decompositions for CQC hardware, and computed the resource requirements (i.e., number of photon-number states) for achieving a desired accuracy in the classical simulation of continuous-variable quantum programs.

Figures

Figures reproduced from arXiv: 2607.17714 by Stefanie Muroya, Thomas A. Henzinger.

Figure 1
Figure 1. Figure 1: Syntax of CvQPL. JMeas(𝑞)K(𝜌) = Í∞ 𝑖=0 J⟨|𝑖⟩ ⟨𝑖| , 𝑞⟩K(𝜌) JD(𝑞, 𝑟0, 𝑟1)K(𝜌) = J⟨𝑒 (−i √ 2(𝑟0𝑃b−𝑟1𝑋b) ), 𝑞⟩K(𝜌) JS(𝑞, 𝑟)K(𝜌) = J⟨𝑒 ( 𝑟 ( (𝐴b) 2− (𝐴b†) 2 ) 2 ) , 𝑞⟩K(𝜌) JReset(𝑞)K(𝜌) = Í∞ 𝑖=0 J⟨|0⟩ ⟨𝑖| , 𝑞⟩K(𝜌) JR(𝑞, 𝑟)K(𝜌) = J⟨𝑒 (i𝑟𝐴b†𝐴b) , 𝑞⟩K(𝜌) JV(𝑞, 𝑟)K(𝜌) = J⟨𝑒 ( i𝑟𝑋b3 3 ) , 𝑞⟩K(𝜌) JBS(𝑞0, 𝑞1, 𝑟0, 𝑟1)K(𝜌) = J⟨𝑒 (𝑟0 (𝑒 i𝑟1 (𝐴b⊗𝐴b† )−𝑒 −i𝑟1 (𝐴b†⊗𝐴b) ) ) , (𝑞0, 𝑞1)⟩K(𝜌) J𝑃1; 𝑃2K(𝜌) = J𝑃2K(J𝑃1K(𝜌)) [PITH_… view at source ↗
Figure 2
Figure 2. Figure 2: Semantics of CvQPL (each program denotes a function on Schwartz density operators). JD(𝑞, 𝑟0, 𝑟1)K ∗ (𝑋b𝑞) = 𝑋b𝑞 + √ 2𝑟0I JD(𝑞, 𝑟0, 𝑟1)K ∗ (𝑃b𝑞) = 𝑃b𝑞 + √ 2𝑟1I JR(𝑞, 𝑟)K ∗ (𝑋b𝑞) = 𝑋b𝑞 · cos(𝑟) − 𝑃b𝑞 · sin(𝑟) JR(𝑞, 𝑟)K ∗ (𝑃b𝑞) = 𝑃b𝑞 · cos(𝑟) + 𝑋b𝑞 · sin(𝑟) JBS(𝑞0, 𝑞1, 𝑟0, 𝑟1)K ∗ (𝑋b𝑞0 ) = 𝑋b𝑞0 cos(𝑟0) − sin(𝑟0) (𝑋b𝑞1 cos(𝑟1) + 𝑃b𝑞1 sin(𝑟1)) JS(𝑞, 𝑟)K ∗ (𝑋b𝑞) = 𝑒 −𝑟 · 𝑋b𝑞 JBS(𝑞0, 𝑞1, 𝑟0, 𝑟1)K ∗ (𝑃b𝑞0 ) = 𝑃b𝑞… view at source ↗
Figure 3
Figure 3. Figure 3: Semantics of the dual of unitary atomic programs for the canonical observables (the dual of each [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Syntax of quantum terms and assertions. The syntax of quantum terms and assertions is shown in Figures 4 and 5. A quantum term 𝜏 ∈ T denotes an observable expressible as a polynomial over the canonical operators. Although the syntax implicitly permits only complex constants with a finite symbolic representation, it also [PITH_FULL_IMAGE:figures/full_fig_p015_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Semantics of quantum terms and assertions, where [PITH_FULL_IMAGE:figures/full_fig_p016_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Syntax of expanded quantum terms over ladder operators. [PITH_FULL_IMAGE:figures/full_fig_p017_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Proof system for CvQHL. Theorem 2. Let ⊢ denote syntactic derivability using the proof system of [PITH_FULL_IMAGE:figures/full_fig_p019_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Hoare triple for the program HomodyneMeas(𝑟) that measures the position of 𝑞0 via Fock measure￾ments using an ancilla 𝑞1. The weakest precondition characterizes both the expected position and its variance. While the expectation is exact for every displacement 𝑟, the quadratic observable reveals an additional single-shot noise term that decreases as 1/𝑟 2 . 5.1.3 Superdense coding [3, 12, 14]. Superdense co… view at source ↗
Figure 9
Figure 9. Figure 9: (a) Hoare triple for the continuous-variable Deutsch–Jozsa program [PITH_FULL_IMAGE:figures/full_fig_p022_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Hoare triple for the SuperdenseCoding(𝑟, 𝑥, 𝑝) program, with squeezing parameter 𝑟, and two real numbers (x, p) that correspond to the message that Alice (𝑞0) wants to send to Bob (𝑞1). The derived weakest precondition proves that Bob recovers the encoded position and momentum values while quantifying the finite-squeezing variance, which decreases as 𝑒 −2𝑟 /2. 5.2 Program equivalence In this subsection, w… view at source ↗
Figure 11
Figure 11. Figure 11: On the left, we have the weakest precondition derived to determine how the expectation value of the [PITH_FULL_IMAGE:figures/full_fig_p025_11.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

58 extracted references · 9 linked inside Pith

  1. [1]

    Aghaee Rad, Thomas Ainsworth, Rafael N

    H. Aghaee Rad, Thomas Ainsworth, Rafael N. Alexander, Brandon Altieri, Mohsen F. Askarani, R. Baby, Leonardo Banchi, Ben Q. Baragiola, J. Eli Bourassa, R. S. Chadwick, et al. 2025. Scaling and networking a modular photonic quantum computer.Nature638, 8052 (2025), 912–919

    2025

  2. [2]

    Ballentine

    Leslie E. Ballentine. 2014.Quantum mechanics: a modern development. World Scientific Publishing Company, Singapore

    2014

  3. [3]

    Masashi Ban. 1999. Quantum dense coding via a two-mode squeezed-vacuum state.JOptB1, 6 (1999), L9–L11

    1999

  4. [4]

    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. arXiv:2510.07051 [quant-ph] https://arxiv.org/abs/2510.07051

    Pith/arXiv arXiv 2026

  5. [5]

    Jeremy Becnel and Ambar Sengupta. 2015. The Schwartz space: Tools for quantum mechanics and infinite dimensional analysis.Mathematics3, 2 (2015), 527–562

    2015

  6. [6]

    Bennett, Gilles Brassard, Claude Crépeau, Richard Jozsa, Asher Peres, and William K

    Charles H. Bennett, Gilles Brassard, Claude Crépeau, Richard Jozsa, Asher Peres, and William K. Wootters. 1993. Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels.Physical Review Letters70, 13 (March 1993), 1895–1899. doi:10.1103/PhysRevLett.70.1895

    doi:10.1103/physrevlett.70.1895 1993

  7. [7]

    Blanchard, Erwin

    Philippe. Blanchard, Erwin. Brüning, and SpringerLink (Online service). 2015.Mathematical Methods in Physics. Springer International Publishing, San Diego, CA

    2015

  8. [8]

    2013.Concentration Inequalities: A Nonasymptotic Theory of Independence

    Stéphane Boucheron, Gábor Lugosi, and Pascal Massart. 2013.Concentration Inequalities: A Nonasymptotic Theory of Independence. Oxford University Press, Oxford, UK

    2013

  9. [9]

    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, et al. 2021. Blueprint for a scalable photonic fault-tolerant quantum computer.Quantum5 (2021), 392

    2021

  10. [10]

    Jonatan Bohr Brask. 2022. Gaussian states and operations – a quick reference. arXiv:2102.05748 [quant-ph]

    Pith/arXiv arXiv 2022

  11. [11]

    Braunstein and H

    Samuel L. Braunstein and H. J. Kimble. 1998. Teleportation of Continuous Quantum Variables.Physical Review Letters 80 (Jan 1998), 869–872. Issue 4. doi:10.1103/PhysRevLett.80.869

    doi:10.1103/physrevlett.80.869 1998

  12. [12]

    Samuel L Braunstein and H Jeff Kimble. 2000. Dense coding for continuous variables.Physical Review A61, 4 (2000), 042302

    2000

  13. [13]

    2003.Quantum information with continuous variables

    Samuel L Braunstein and Arun K Pati. 2003.Quantum information with continuous variables. Springer Dordrecht, Dordrecht, Netherlands

    2003

  14. [14]

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

    2005

  15. [15]

    Samantha Buck, Robin Coleman, and Hayk Sargsyan. 2021. Continuous variable quantum algorithms: an introduction. arXiv:2107.02151 [quant-ph]

    Pith/arXiv arXiv 2021

  16. [16]

    Gabriele Carcassi, Francisco Calderón, and Christine A. Aidala. 2025. The unphysicality of Hilbert spaces.Quantum Studies: Mathematics and Foundations12, 1 (2025), 13

    2025

  17. [17]

    Sophie Choe. 2022. Quantum computing overview: discrete vs. continuous variable models. arXiv:2206.07246 [quant- ph]

    Pith/arXiv arXiv 2022

  18. [18]

    Man-Duen Choi. 1975. Completely positive linear maps on complex matrices.LAA10, 3 (1975), 285–290. doi:10.1016/ 0024-3795(75)90075-0

    1975

  19. [19]

    2011.Symplectic methods in harmonic analysis and in mathematical physics

    Maurice A De Gosson. 2011.Symplectic methods in harmonic analysis and in mathematical physics. Vol. 7. Springer Science & Business Media, Basel, Switzerland

    2011

  20. [20]

    David Deutsch and Richard Jozsa. 1992. Rapid solution of problems by quantum computation.Proceedings of the Royal Society of London. Series A: Mathematical and Physical Sciences439, 1907 (1992), 553–558. doi:10.1098/rspa.1992.0167

    arXiv 1992

  21. [21]

    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

  22. [22]

    GB FOLLAND. 1989. HARMONIC-ANALYSIS IN PHASE-SPACE.AMS122 (1989), 1–+

    1989

  23. [23]

    2011.Quantum teleportation and entanglement: a hybrid approach to optical quantum information processing

    Akira Furusawa and Peter Van Loock. 2011.Quantum teleportation and entanglement: a hybrid approach to optical quantum information processing. John Wiley & Sons, New Jersey, USA

    2011

  24. [24]

    Operator Theory: Advances and Applications

    M de Gosson Symplectic Geometry and Quantum Mechanics. 2006. Birkhäuser, Basel, series “Operator Theory: Advances and Applications”(subseries:“Advances in Partial Differential Equations”)

    2006

  25. [25]

    François Gieres. 2000. Mathematical surprises and Dirac’s formalism in quantum mechanics.RoPP63, 12 (2000), 1893–1931

    2000

  26. [26]

    Daniel Gottesman, Alexei Kitaev, and John Preskill. 2000. Encoding a qubit in an oscillator. arXiv:10.1103 [quant-ph]

    2000

  27. [27]

    Alex Graves, Greg Wayne, and Ivo Danihelka. 2014. Neural Turing machines. arXiv:1410.5401 [cs.NE]

    Pith/arXiv arXiv 2014

  28. [28]

    Alex Graves, Greg Wayne, Malcolm Reynolds, Tim Harley, Ivo Danihelka, Agnieszka Grabska-Barwińska, Sergio Gómez Colmenarejo, Edward Grefenstette, Tiago Ramalho, John Agapiou, et al . 2016. Hybrid computing using a neural Formal Verification of Continuous-Variable Quantum Programs 27 network with dynamic external memory.Nature538, 7626 (2016), 471–476

    2016

  29. [29]

    Brian C. Hall. 2013.Quantum theory for mathematicians. Springer, New York, USA

    2013

  30. [30]

    Richard V. Kadison. 1951. Order Properties of Bounded Self-Adjoint Operators.PAMS2, 3 (1951), 505–510

    1951

  31. [31]

    Nathan Killoran, Josh Izaac, Nicolás Quesada, Ville Bergholm, Matthew Amy, and Christian Weedbrook. 2019. Straw- berry Fields: A software platform for photonic quantum computing.Quantum3 (March 2019), 129. doi:10.22331/q- 2019-03-11-129

    doi:10.22331/q- 2019

  32. [32]

    Pieter Kok and Brendon W. Lovett. 2010.Introduction to optical quantum information processing. Cambridge University Press, Cambridge, UK

    2010

  33. [33]

    Larsen, J

    Mikkel V. Larsen, J. Eli Bourassa, Sacha Kocsis, Joel F. Tasker, Robert S. Chadwick, Carlos González-Arciniegas, Jacob Hastrup, Carlos E. Lopetegui-González, Filippo M. Miatto, A. Motamedi, et al. 2025. Integrated photonic source of Gottesman–Kitaev–Preskill qubits.Nature642, 8068 (2025), 587–591

    2025

  34. [34]

    Ulf Leonhardt and Harry Paul. 1995. Measuring the quantum state of light.PQE19, 2 (1995), 89–130

    1995

  35. [35]

    Junyi Liu, Bohua Zhan, Shuying Unruh, Mingsheng Ying, and Naijun Zhan. 2019. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. InCA V. Springer International Publishing, New York, USA, 187–206

    2019

  36. [36]

    Seth Lloyd. 2003. Hybrid quantum computing. InQuantum information with continuous variables. Springer, Dordrecht, 37–45

    2003

  37. [37]

    Braunstein

    Seth Lloyd and Samuel L. Braunstein. 1999. Quantum computation over continuous variables.Physical Review Letters 82, 8 (1999), 1784

    1999

  38. [38]

    Yoshichika Miwa, Jun-ichi Yoshikawa, Peter van Loock, and Akira Furusawa. 2009. Demonstration of a universal one-way quantum quadratic phase gate.Physical Review A80, 5 (2009), 050303

    2009

  39. [39]

    Hironari Nagayoshi, Warit Asavanant, Ryuhoh Ide, Kosuke Fukui, Atsushi Sakaguchi, Jun-ichi Yoshikawa, Nicolas C Menicucci, and Akira Furusawa. 2025. ZX graphical calculus for continuous-variable quantum processes.Physical Review Research7, 3 (2025), 033141

    2025

  40. [40]

    Nielsen and Isaac L

    Michael A. Nielsen and Isaac L. Chuang. 2010.Quantum Computation and Quantum Information. Cambridge University Press, Cambridge, UK

    2010

  41. [41]

    Niloofar Parviz, Maedeh Dolati, and Nojan Behzadi Alam. 2024. Some impressive properties of unbounded operators in quantum mechanics.LAJPE18, 1 (2024), 1302

    2024

  42. [42]

    Andriamanankasina Ramanantoanina and Tamás Titkos. 2024. Lattice properties of strength functions.ASM90, 3-4 (2024), 1–11

    2024

  43. [43]

    2012.Methods of modern mathematical physics: Functional analysis

    Michael Reed. 2012.Methods of modern mathematical physics: Functional analysis. Elsevier, New York, USA

    2012

  44. [44]

    Paul Renault, Patrick Yard, Raphael C Pooser, Miller Eaton, and Hussain Asim Zaidi. 2025. End-to-end switchless architecture for fault-tolerant photonic quantum computing.Quantum9 (2025), 1796

    2025

  45. [45]

    Federico Rueda and Sonia Lopez Alarcon. 2021. Continuous Variable Quantum Compilation. InCSCI. IEEE, Las Vegas, NV, USA, 1765–1770. doi:10.1109/CSCI54926.2021.00335

    arXiv 2021

  46. [46]

    J. J. Sakurai and Jim Napolitano. 2020.Modern Quantum Mechanics. Cambridge University Press, Cambridge, UK

    2020

  47. [47]

    Laurent Schwartz. 1957. Théorie des distributions à valeurs vectorielles. I. InAnnales de l’institut Fourier, Vol. 7. Institut Fourier, Grenoble, France, 1–141

    1957

  48. [48]

    2023.Quantum continuous variables: a primer of theoretical methods

    Alessio Serafini. 2023.Quantum continuous variables: a primer of theoretical methods. CRC Press, Boca Raton, FL

    2023

  49. [49]

    Shaikh, Lia Yeh, and Stefano Gogioso

    Razin A. Shaikh, Lia Yeh, and Stefano Gogioso. 2024. The Focked-up ZX Calculus: Picturing Continuous-Variable Quantum Computation. arXiv:2406.02905 [quant-ph]

    Pith/arXiv arXiv 2024

  50. [50]

    Xin Sun, Xingchi Su, Xiaoning Bian, and Huiwen Wu. 2024. On the Relative Completeness of Satisfaction-based Quantum Hoare Logic. arXiv:2405.01940 [quant-ph]

    Pith/arXiv arXiv 2024

  51. [51]

    Aarthi Sundaram, Robert Rand, Kartik Singhal, and Brad Lackey. 2022. Hoare meets Heisenberg: A lightweight logic for quantum programs. arXiv:2101.08939 [quant-ph]

    Pith/arXiv arXiv 2022

  52. [52]

    J. v. Neumann. 1931. Die Eindeutigkeit der Schrödingerschen Operatoren.Math. Ann.104, 1 (1931), 570–578. doi:10.1007/BF01457956

    doi:10.1007/bf01457956 1931

  53. [53]

    Xiaoguang Wang. 2001. Continuous-variable and hybrid quantum gates.JPhysA34, 44 (Oct. 2001), 9577. doi:10.1088/ 0305-4470/34/44/316

    2001

  54. [54]

    Cerf, Timothy C

    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.RMP84, 2 (2012), 621–669

    2012

  55. [55]

    Mingsheng Ying. 2012. Floyd–Hoare logic for quantum programs.TOPLAS33, 6 (2012), 19:1–19:49. doi:10.1145/ 2049706.2049708

    arXiv 2012

  56. [56]

    Mingsheng Ying. 2024. A Practical Quantum Hoare Logic with Classical Variables, I. arXiv:2412.09869 [quant-ph]

    Pith/arXiv arXiv 2024

  57. [57]

    Han-Sen Zhong, Hui Wang, Yu-Hao Deng, Ming-Cheng Chen, Li-Chao Peng, Yi-Han Luo, Jian Qin, Dian Wu, Xing Ding, Yi Hu, Peng Hu, Xiao-Yan Yang, Wei-Jun Zhang, Hao Li, Yuxuan Li, Xiao Jiang, Lin Gan, Guangwen Yang, Lixing You, Zhen Wang, Li Li, Nai-Le Liu, Chao-Yang Lu, and Jian-Wei Pan. 2020. Quantum computational advantage using photons.Science370, 6523 (2...

    doi:10.1126/science.abe8770 2020

  58. [58]

    Li Zhou, Nengkun Yu, and Mingsheng Ying. 2019. An Applied Quantum Hoare Logic. InPLDI (PLDI ’19). ACM, New York, USA, 1149–1162. doi:10.1145/3314221.3314584 Formal Verification of Continuous-Variable Quantum Programs 29 7 Appendix 7.1 Appendix: proofs of propositions 7.1.1 Appendix: Polynomial ladder operators normal-ordering (Proposition 4). Proposition ...

    arXiv 2019