Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions

T0 review · 3 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash

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

Pith's one-line read cqOTL is the first sound and complete relational logic for classical-quantum programs, with completeness resting on a new duality theorem for hybrid quantum states with unbounded assertions.

desk verdict Genuine contribution, but the main completeness theorem is not established: the coupling compactness lemma is false, and the structural rules rest on it. read the letter →

arxiv 2510.07051 v2 pith:U2WZOTL7 submitted 2025-10-08 quant-ph cs.LOcs.PL

Gilles Barthe , Minbo Gao , Jam Kabeer Ali Khan , Matthijs Muis , Ivan Renison , Keiya Sakabe , Michael Walter , Yingte Xu
show 2 more authors
Tianshi Yu Li Zhou
This is my paper · ORCID
classification quant-phcs.LOcs.PL MSC 68Q6081P6849Q2290C46
keywords classical-quantumprogramsrelationalHoarelogicdualitytheoremunboundedassertionscouplingsoptimaltransportcompletenessquantumverification
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper settles a standing question: can relational reasoning about hybrid classical-quantum programs be complete, so that every semantically valid judgment has a proof? The authors present cqOTL, a relational program logic for the cqWhile language, and prove that for almost-surely terminating programs every valid judgment — including those with unbounded, infinite-valued relational assertions over countably infinite classical state spaces — is derivable. The result rests on a duality theorem for classical-quantum states: the minimal expected value of an assertion over all couplings of two states equals a supremum over split assertions on the marginals, a hybrid analogue of classical optimal-transport duality. This identity lets the logic reduce arbitrary relational reasoning to non-relational weakest-preconditions. If correct, cqOTL is the first relational logic with unconditional completeness for quantum or classical-quantum programs, and the same theorem upgrades the probabilistic logic eRHL and the quantum logic qOTL to full unbounded completeness.

What carries the argument

The central object is the duality set Y(φ) of a relational assertion φ: triples (n, φ1, φ2) with bounded unary assertions φ1, φ2 such that φ1⊗id + id⊗φ2 ⊑ φ + n·id. The duality identity — the infimum of E[φ] over all couplings equals the supremum of E[φ1]+E[φ2]−n over Y(φ) — converts any postcondition into a split one, where weakest-precondition reasoning applies. Its proof uses conic-programming duality on finite classical spaces, then a norm bound (Lemma B.4) on ε-approximate maximizers of the dual program that depends only on ‖φ‖ and ε — not on the size of the classical space or Hilbert-space dimension — which controls the approximation error when passing from finite subsets to the full c

What would settle it

Exhibit a pair of classical-quantum states of equal total mass and a bounded assertion φ such that the infimum of EΔ[φ] over all couplings strictly exceeds the supremum of EΔ1[φ1]+EΔ2[φ2]−n over split assertions — a duality gap contradicting Theorem 8.11 and, with it, completeness. A more targeted check: build a sequence of approximate couplings of two subnormalized states with no convergent subsequence, which would break the cited compactness lemma that the limit rules depend on.

Watch

Extended reading notes

Core claim

The central claim is Theorem 8.2: for HAST cqWhile commands c1, c2 and any unbounded relational assertion φ, semantic validity ⊨{ψ}c1∼c2{φ} implies derivability ⊢{ψ}c1∼c2{φ} in cqOTL. The engine is the classical-quantum duality theorem (Theorem 8.11): for states Δ1, Δ2 with equal total mass and bounded φ, the infimum of EΔ[φ] over couplings Δ equals the supremum of EΔ1[φ1]+EΔ2[φ2]−n over bounded split assertions φ1⊗id+id⊗φ2 ⊑ φ+n·id. Countably infinite classical state spaces rule out merely combining classical and finite-dimensional quantum duality; the proof adds a dimension-independent norm bound on ε-approximate dual optimizers and takes a finite-to-countable limit. The same duality gives

Load-bearing premise

Soundness of the limit, consequence, and unbounded-duality rules presupposes that the set of couplings of two classical-quantum states is compact in the trace-norm topology, with the expectation function lower semicontinuous — a fact the paper takes from the literature rather than proving; if compactness fails for countably infinite classical support or subnormalized states, the convergent-subsequence arguments that promote approximate couplings to exact ones collapse.

Editorial extensions

If this is right

  • cqOTL becomes the first relational logic with unconditional completeness for classical-quantum programs: every valid relational judgment, including unbounded quantitative assertions, has a proof.
  • The new unbounded duality rule removes prior boundedness restrictions: eRHL for probabilistic programs and qOTL for quantum programs are each sound and complete for arbitrary infinite-valued postconditions.
  • The unified coupling condition for sampling and measurement lets the logic relate programs whose random draws and measurements are misaligned, such as a Bernoulli sample matched against two qubit measurements.
  • The authors report a machine-checked prototype (~2.5K lines) suggesting the proof obligations can be mechanized, a step toward verification of post-quantum cryptography on a complete logical foundation.

Reading between the lines

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

  • If the duality theorem is correct, it is likely to be useful beyond verification — hybrid classical-quantum optimal transport has lacked such an identity, and the claimed extension to infinite-dimensional density operators is a natural statement to verify.
  • Completeness moves the practical bottleneck from constructing couplings to discharging assertion-level math, so decision procedures for Dirac notation, orthomodular logic, and classical theories become the gating technology for tool support.
  • A testable extension: the same finite-approximation technique should yield duality for classical state spaces beyond countable sets (e.g., measurable spaces), provided the compactness of couplings holds there — a reader could check whether the subnormalized-state compactness needs a genuinely new proof.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper develops cqOTL, a sound and complete relational program logic for a classical-quantum while language (cqWhile) with unbounded, infinite-valued assertions. Judgments {ψ} c1 ∼ c2 {φ} are interpreted over state couplings: validity requires that for every input coupling there is an output coupling satisfying E[φ] ≤ E[ψ]. The proof system combines one-sided and two-sided rules with structural rules [Conseq], [Limit], and [Unbounded-Duality]. Completeness is obtained by first proving completeness for split postconditions via non-relational weakest preconditions, then using a Kantorovich–Rubinstein-type duality theorem (Theorem 8.11 / B.1) to reduce arbitrary postconditions to split ones. The appendix contains detailed proofs of the duality theorem, convergence results, soundness, and completeness, and the paper also derives completeness for pWhile and qWhile with unbounded assertions.

Significance. If the results are correct, Theorem 8.2 is a significant advance: it would be the first unconditional completeness theorem for a relational logic covering classical-quantum programs, improving on prior bounded-postcondition results [4, 10]. The duality theorem for hybrid classical-quantum states, with its dimension-independent norm bound, is a contribution of independent interest in quantum optimal transport. The paper is unusually detailed: the main duality proof is carried out in the appendix, and the proof system is exercised on nontrivial examples including deferred measurement and rejection sampling. However, the claimed scope is broader than the formal development, and two load-bearing proof points—the use of the duality theorem for subnormalized states and the proof of the coupling compactness lemma—need repair.

major comments (3)
  1. [Abstract, Section 3, Appendix B] The title and abstract claim a logic for 'infinite-dimensional quantum programs' and 'infinite-dimensional duality theorems for infinite-dimensional quantum states,' but Section 3 explicitly says 'We only consider finite-dimensional Hilbert spaces,' and Theorem 8.11/B.1 is stated for finite-dimensional H1, H2. Appendix B further says the extension to general infinite-dimensional quantum density operators is deferred. The paper's actual infinite-dimensionality is in the countable classical state spaces and in unbounded assertions, not in the quantum registers. This overclaim should be corrected in the title/abstract or the results must be genuinely extended.
  2. [Appendix F, soundness of [Unbounded-Duality]] Theorem B.1 is stated only for states with tr(Δ1)=tr(Δ2)=1. In the soundness proof of [Unbounded-Duality], the proof applies this theorem to Δ'_1 = ⟦c1⟧(|σ1,tr2(ρ)|) and Δ'_2 = ⟦c2⟧(|σ2,tr1(ρ)|), whose common trace is t = tr(ρ), which can be strictly less than 1. The displayed manipulation 'tr(ψ(σ1,σ2)ρ) + n ≥ sup ...' should read 'tr(ψρ) + n·t ≥ ...', and the duality theorem then gives sup(E[φ1]+E[φ2] − n·t), not −n. A normalization/scaling argument for subnormalized states is needed. As written, the proof of soundness of this central rule is incomplete.
  3. [Appendix C, Lemma C.2] Lemma C.2 asserts trace-norm compactness of the set of couplings and cites Friedland–Ge–Zhi Theorem 1.4 as an immediate corollary. That theorem cannot imply trace-norm compactness of all couplings in a separable Hilbert space, since the trace-class unit ball of an infinite-dimensional Hilbert space is not trace-norm compact. In the present setting (finite-dimensional H, countable A) the lemma is in fact true and can be proved directly by a total-boundedness/truncation argument, but the supplied proof is not valid. This matters because the soundness proofs of [Conseq], [Limit], and [Unbounded-Duality] all rely on the compactness of the coupling set to turn approximate witnesses into exact ones. The proof must be replaced by a correct direct argument. (For completeness: the specific transposition counterexample that has been circulated does not refute the lemma—the proposed γ_n have second
minor comments (5)
  1. [Definition 5.4] The definition of state coupling has a typo: it says 'Δ1 ∈ S(A2,H1)' and 'Δ2 ∈ S(A2,H2)'; the first should be S(A1,H1).
  2. [Section 5.2] The paragraph introducing CVarrel and cStatesrel is repeated almost verbatim; one copy should be deleted.
  3. [Propositions 8.12 and 8.13] The headings read 'Classical-qantum monotone convergence' and 'Classical-qantum Fatou’s lemma'—likely typos for 'classical-quantum.'
  4. [Section 4.3] The definition of HAST reads awkwardly: 'almost-surely terminating, written c∈AST, if it is trace-preserving, and hereditarily trace-preserving, written c∈HAST, if all its sub-programs are.' It should explicitly say that HAST means all subprograms are AST/trace-preserving.
  5. [Appendix C, Lemma C.2] The proof of Lemma C.2 should either prove the total-boundedness argument or cite a theorem that actually gives trace-norm compactness for the block-diagonal sub-class of couplings used here.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; soundness and completeness use a standard separation of concerns and independent duality proof.

full rationale

The central completeness theorem (Theorem 8.2) is built on the [Unbounded-Duality] rule, whose soundness is proved separately in Appendix F via Theorem B.1 (the duality theorem). Theorem B.1 is proved in Section B by conic/semidefinite programming duality for finite sets, a dimension-independent norm bound (Lemma B.4), and a finite-approximation argument; it does not invoke the logic or the completeness result. Lemma 8.8, used in completeness, is a direct monotonicity argument from the definition of the duality set Y(φ): if φ1⊗id+id⊗φ2 ⊑ φ+n·id, then semantic validity for φ implies semantic validity for the split postcondition with precondition ψ+n·id. This is not the rule being assumed; it is the verification of the rule's hypotheses. The only self-citation [10] supplies background constructions (infinite-valued observables, finite-dimensional quantum duality) and is not load-bearing: the main proof of Lemma B.3 uses conic duality, and the citation to [10] is explicitly an alternative ('One can also establish ...'). The compactness lemma (Lemma C.2) is cited to external [Friedland et al. 2020] and is used to make infima into minima and extract convergent subsequences; whether that citation is mathematically sufficient is a correctness/soundness concern, not a circularity, because it does not reduce the theorem to its own conclusion. Accordingly, no fitted parameters, no prediction renamed from fit, and no definition of the target in terms of itself appear.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The central claim rests on standard convex/operator-theoretic machinery and several domain assumptions: finite-dimensional quantum Hilbert spaces, countable classical state spaces, trace-preserving termination, and external compactness/duality theorems. No fitted parameters or invented physical entities are introduced.

assumptions (6)
  • domain assumption All quantum Hilbert spaces are finite-dimensional.
    Section 3 states 'We only consider finite-dimensional Hilbert spaces.' The abstract says infinite-dimensional quantum programs, but the formal theorems and proofs do not cover infinite-dimensional quantum registers.
  • domain assumption Classical variable state spaces are countable and states are subnormalized with trace ≤ 1.
    Definition 4.4 defines cqStates as functions from cStates to D(H_QVar) with total trace ≤ 1. This is needed for the summations, truncations, and coupling arguments in the paper.
  • domain assumption Meta-theorems are restricted to HAST (hereditarily almost-surely terminating) commands.
    Soundness and completeness, Theorems 8.1 and 8.2, quantify over HAST commands; many proof rules need trace-preservation side-conditions, so the completeness claim does not cover diverging programs.
  • standard math The set of couplings with fixed marginals is compact in the trace-norm topology.
    Appendix C Lemma C.2, attributed to [Friedland et al. 2020], is used in the soundness proofs of [Limit], [Conseq], and [Unbounded-Duality]. It is load-bearing and not proved in the paper.
  • standard math Finite-dimensional conic/Slater duality holds for the finite classical-state case.
    Appendix B Lemma B.3 proves the finite-case duality via conic programming and Slater's theorem; strict feasibility is checked, but the external duality theorem is assumed.
  • domain assumption Infinite-valued predicate algebra from prior work extends to the classical-quantum setting.
    Section 3 and Appendix A import Pos∞ operations, truncation, and algebraic identities from [10]. The logic's unbounded assertions depend on this extension.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions." pith.science (2026). https://pith.science/paper/U2WZOTL7

@misc{pith2026251007051,
  author       = {Pith},
  title        = {Pith review of: Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/U2WZOTL7}},
  note         = {Machine review of arXiv:2510.07051}
}
read the original abstract

We present sound and complete relational program logics for infinite-dimensional quantum and classical-quantum programs. The logics model assertions as self-adjoint unbounded linear relations, which simultaneously support quantitative and qualitative reasoning. Our main theoretical results include new convergence theorems and infinite-dimensional duality theorems for infinite-dimensional quantum states, which we use to establish completeness.

Figures

Figures reproduced from arXiv: 2510.07051 by the authors.

Figure 1
Figure 1. Comparison with prior logics. We use ✔X when completeness holds for post-conditions verifying 𝑋. Ours results are shown in blue. We use b/u-duality for our bounded and unbounded duality rules. the problem of relational verification, whose goal is to relate two programs, or two executions of the same program—thus relational properties are a special case of hyper-properties [24]. Relational properties encompass many p… view at source ↗
Figure 2
Figure 2. Program walk (Left) is a classical random walk. Program walk-meas (Right) is a quantum-classic equivalent where each step is given by the outcome of a quantum measurement—not a quantum random walk. ⊢ {𝑥1 = 𝑥2 } skip ∼ skip {𝑥1 = 𝑥2 ∧ Í 𝑖 |𝑖⟩𝑞2 ⟨+| 𝜙 |+⟩𝑞2 ⟨𝑖| } [Init-R] ⊢ {𝑥1 = 𝑥2 } skip ∼ 𝑞2 := |+⟩ {𝑥1 = 𝑥2 ∧ |+⟩𝑞2 ⟨+| } [Measure-Sample] ⊢ {𝑥1 = 𝑥2 } 𝑏1 ←$ {0, 1} ∼ 𝑞2 := |+⟩;𝑏2 ← meas (𝑃0, 𝑃1 ) [𝑞2 ] {𝑥1 = 𝑥2 ∧ 𝑏1 … view at source ↗
Figure 3
Figure 3. Derivation of illustrative example. [Init-R] is symmetric to [Init-L]. Finally, Section 9 presents related work and Section 10 provides perspectives for future work. 2 ILLUSTRATIVE EXAMPLE [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: Selected one-sided rules. We display left rules. Each rule has a symmetric right rule. [PITH_FULL_IMAGE:figures/full_fig_p015_4.png]
Figure 5
Figure 5. Figure 5: Selected two-sided rules [PITH_FULL_IMAGE:figures/full_fig_p016_5.png]
Figure 6
Figure 6. Figure 6: Structural rules. of 𝜇1 and 𝜇2. Moreover, the following rule, which is an instance of our [Sample] rule, improves marginally but usefully on the sampling rule in [4] (the latter is given in a probabilistic setting, but this is unimportant here), by allowing to guarded …
Figure 7
Figure 7. Figure 7: Deferred measurement judgement: Circuit-1 (Left) and Circuit-2 (Right). [PITH_FULL_IMAGE:figures/full_fig_p018_7.png]
Figure 8
Figure 8. Figure 8: Equivalence judgement of Rejection Sampling (Left) and Bit-flip (Right). [PITH_FULL_IMAGE:figures/full_fig_p019_8.png]
Figure 9
Figure 9. Figure 9: Qubit flipping judgement. , Vol. 1, No. 1, Article . Publication date: October 2025 [PITH_FULL_IMAGE:figures/full_fig_p019_9.png]
Figure 10
Figure 10. Figure 10: Bernoulli samplers judgement: Bern-1 (Left) and Bern-2 (Right). Our final example exercises the duality rule. It involves two programs shown in [PITH_FULL_IMAGE:figures/full_fig_p020_10.png]
Figure 11
Figure 11. Figure 11: Structural representation of ⟦𝑐⟧. Lemma E.2 (Partial trace of simple state). For every 𝑎1 ∈ A1, 𝑎2 ∈ A2, 𝜌 ∈ D (H1 ⊗ H2), then we have tr2 (| (𝑎1, 𝑎2), 𝜌|) = (|𝑎1, tr2 (𝜌)|), tr1 (| (𝑎1, 𝑎2), 𝜌|) = (|𝑎2, tr1 (𝜌)|). Lemma E.3 (Expectation of simple state). For every 𝑎 …

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Formal Verification of Continuous-Variable Quantum Programs

    quant-ph 2026-07 conditional novelty 8.0 of 10

    A sound and relatively complete Hoare logic for continuous-variable quantum programs, with polynomial assertions and an automated weakest-precondition calculator.

Reference graph

Works this paper leans on

73 extracted references · 5 canonical work pages · cited by 1 Pith paper

  1. [1]

    Aliprantis and Kim C

    Charalambos D. Aliprantis and Kim C. Border. 2006.Infinite Dimensional Analysis. Springer-Verlag, Berlin/Heidelberg. https://doi.org/10.1007/3-540-29587-9

    doi:10.1007/3-540-29587-9 2006

  2. [2]

    José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, and Pierre-Yves Strub. 2024. Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-K...

    2024

  3. [3]

    Andris Ambainis, Mike Hamburg, and Dominique Unruh. 2019. Quantum security proofs using semi-classical oracles. InAdvances in Cryptology–CRYPTO 2019: 39th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 18–22, 2019, Proceedings, Part II 39. Springer, 269–295

    2019

  4. [4]

    Martin Avanzini, Gilles Barthe, Davide Davoli, and Benjamin Grégoire. 2025. A Quantitative Probabilistic Relational Hoare Logic.Proc. ACM Program. Lang.9, POPL (2025), 1167–1195. https://doi.org/10.1145/3704876

    doi:10.1145/3704876 2025

  5. [5]

    Jialu Bao, Emanuele D’Osualdo, and Azadeh Farzan. 2025. Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning.Proc. ACM Program. Lang.9, POPL (2025), 1719–1749. https://doi.org/10.1145/3704894

    doi:10.1145/3704894 2025

  6. [6]

    Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, and Xiaodi Wu. 2023. Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. InAdvances in Cryptology - CRYPTO 2023 - 43rd Annual International Cryptology Conference, CRYPTO 2023, Santa Barbara, C...

    2023

  7. [7]

    Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, and Li Zhou. 2021. EasyPQC: Verifying post-quantum cryptography. InProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. 2564–2586

    2021

  8. [8]

    Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, and Pierre-Yves Strub. 2021. Mechanized Proofs of Adversarial Complexity and Application to Universal Composability.IACR Cryptol. ePrint Arch.2021 (2021), 156. https://eprint.iacr.org/2021/156

    2021

Show all 73 references
  1. [9]

    Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. Proving expected sensitivity of probabilistic programs.Proc. ACM Program. Lang.2, POPL (2018), 57:1–57:29. https://doi.org/10.1145/3158145 , Vol. 1, No. 1, Article . Publication date: Oc...

    2018 doi

  2. [10]

    Gilles Barthe, Minbo Gao, Theo Wang, and Li Zhou. 2025. Complete Quantum Relational Hoare Logics from Optimal Transport Duality.CoRRabs/2501.15238 (2025). https://doi.org/10.48550/ARXIV.2501.15238 arXiv:2501.15238 To appear in Proceedings of LICS 2025

    2025 doi arXiv

  3. [11]

    Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2009. Formal certification of code-based cryptographic proofs. InProceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, Zho...

    2009

  4. [12]

    Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. 2011. Computer-aided security proofs for the working cryptographer. InAnnual Cryptology Conference. Springer, 71–90

    2011

  5. [13]

    Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. 2019. Relational Proofs for Quantum Programs. Proc. ACM Program. Lang.4, POPL, Article 21 (Dec. 2019), 29 pages. https://doi.org/10.1145/3371089

    2019 doi

  6. [14]

    Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella-Béguelin. 2012. Probabilistic relational reasoning for differential privacy. InProceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, U...

    2012

  7. [15]

    Gilles Barthe and Federico Olmedo. 2013. Beyond Differential Privacy: Composition Theorems and Relational Logic for f- divergences between Probabilistic Programs. InAutomata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013,...

    2013 doi

  8. [16]

    2001.Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications

    Aharon Ben-Tal and Arkadi Nemirovski. 2001.Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications. SIAM

    2001

  9. [17]

    Charles H Bennett and Gilles Brassard. 2014. Quantum cryptography: Public key distribution and coin tossing. Theoretical computer science560 (2014), 7–11

    2014

  10. [18]

    Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. InProceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, Neil D. Jones and Xavier Leroy...

    2004

  11. [19]

    1985.Orthomodular Lattices

    Ladislav Beran. 1985.Orthomodular Lattices. Springer Netherlands, Dordrecht. https://doi.org/10.1007/978-94-009- 5215-7

    1985 doi

  12. [20]

    Bernstein, Andreas Hülsing, Stefan Kölbl, Ruben Niederhagen, Joost Rijneveld, and Peter Schwabe

    Daniel J. Bernstein, Andreas Hülsing, Stefan Kölbl, Ruben Niederhagen, Joost Rijneveld, and Peter Schwabe. 2019. The SPHINCS+ Signature Framework.IACR Cryptol. ePrint Arch.(2019), 1086. https://eprint.iacr.org/2019/1086

    2019

  13. [21]

    Dan Boneh, Özgür Dagdelen, Marc Fischlin, Anja Lehmann, Christian Schaffner, and Mark Zhandry. 2011. Random oracles in a quantum world. InAdvances in Cryptology–ASIACRYPT 2011: 17th International Conference on the Theory and Application of Cryptology and Information Security, ...

    2011

  14. [22]

    Bos, Léo Ducas, Eike Kiltz, Tancrède Lepoint, Vadim Lyubashevsky, John M

    Joppe W. Bos, Léo Ducas, Eike Kiltz, Tancrède Lepoint, Vadim Lyubashevsky, John M. Schanck, Peter Schwabe, Gregor Seiler, and Damien Stehlé. 2018. CRYSTALS - Kyber: A CCA-Secure Module-Lattice-Based KEM. In2018 IEEE European Symposium on Security and Privacy, EuroS&P 2018, Lon...

    2018

  15. [23]

    Christophe Chareton, Sébastien Bardin, Dong Ho Lee, Benoît Valiron, Renaud Vilmart, and Zhaowei Xu. 2023. Formal Methods for Quantum Algorithms. InHandbook of Formal Analysis and Verification in Cryptography. CRC Press, 319–422. https://cea.hal.science/cea-04479879

    2023

  16. [24]

    Michael R Clarkson and Fred B Schneider. 2010. Hyperproperties.Journal of Computer Security18, 6 (2010), 1157–1210

    2010

  17. [25]

    Marco Cuturi and Gabriel Peyré. 2019. Computational optimal transport.Found. Trends Mach. Learn11, 5-6 (2019), 355–607

    2019

  18. [26]

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

    2006 doi

  19. [27]

    2006.Multivariate public key cryptosystems

    Jintai Ding, Jason E Gower, and Dieter S Schmidt. 2006.Multivariate public key cryptosystems. Vol. 25. Springer Science & Business Media

    2006

  20. [28]

    Léo Ducas, Eike Kiltz, Tancrède Lepoint, Vadim Lyubashevsky, Peter Schwabe, Gregor Seiler, and Damien Stehlé. 2018. CRYSTALS-Dilithium: A Lattice-Based Digital Signature Scheme.IACR Trans. Cryptogr. Hardw. Embed. Syst.2018, 1 (2018), 238–268. https://doi.org/10.13154/TCHES.V20...

    2018 doi

  21. [29]

    E. A. Feinberg, P. O. Kasyanov, and Y. Liang. 2020. Fatou’s Lemma for Weakly Converging Measures under the Uniform Integrability Condition.Theory of Probability & Its Applications64, 4 (2020), 615–630. https://doi.org/10.1137/ S0040585X97T989738

    2020

  22. [30]

    Yuan Feng and Mingsheng Ying. 2021. Quantum Hoare Logic with Classical Variables.ACM Transactions on Quantum Computing2, 4, Article 16 (Dec. 2021), 43 pages. https://doi.org/10.1145/3456877 , Vol. 1, No. 1, Article . Publication date: October 2025. A Duality Theorem for Classi...

    2021 doi

  23. [31]

    Luis María Ferrer Fioriti and Holger Hermanns. 2015. Probabilistic termination: Soundness, completeness, and compositionality. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 489–501

    2015

  24. [32]

    Pierre-Alain Fouque, Jeffrey Hoffstein, Paul Kirchner, Vadim Lyubashevsky, Thomas Pornin, Thomas Prest, Thomas Ricosset, Gregor Seiler, William Whyte, Zhenfei Zhang, et al. 2018. Falcon: Fast-Fourier lattice-based compact signatures over NTRU.Submission to the NIST’s post-quan...

    2018

  25. [33]

    Shmuel Friedland, Jingtong Ge, and Lihong Zhi. 2020. Quantum Strassen’s theorem.Infinite Dimensional Analysis, Quantum Probability and Related Topics23, 03 (2020), 2050020. https://doi.org/10.1142/S0219025720500204

    2020 doi

  26. [34]

    Haselwarter, Joseph Tassarotti, and Lars Birkedal

    Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. 2024. Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.Proc. ACM Program. Lang.8, POPL (2024), 753–784. https://doi.org/10.1145/3632868

    2024 doi

  27. [35]

    Horn and Fuzhen Zhang

    Roger A. Horn and Fuzhen Zhang. 2005.The Schur Complement and Its Applications. Springer US, Boston, MA, Chapter Basic Properties of the Schur Complement, 17–46. https://doi.org/10.1007/0-387-24273-2_2

    2005 doi

  28. [36]

    Leonid Vasilevich Kantorovich and SG Rubinshtein. 1958. On a space of totally additive functions.Vestnik of the St. Petersburg University: Mathematics13, 7 (1958), 52–59

    1958

  29. [37]

    Juila Kempe. 2003. Quantum random walks: an introductory overview.Contemporary Physics44, 4 (2003), 307–327

    2003

  30. [38]

    Dexter Kozen. 1983. A Probabilistic PDL. InProceedings of the 15th Annual ACM Symposium on Theory of Computing, 25-27 April, 1983, Boston, Massachusetts, USA, David S. Johnson, Ronald Fagin, Michael L. Fredman, David Harel, Richard M. Karp, Nancy A. Lynch, Christos H. Papadimi...

    1983

  31. [39]

    Marco Lewis, Sadegh Soudjani, and Paolo Zuliani. 2023. Formal Verification of Quantum Programs: Theory, Tools, and Challenges.ACM Transactions on Quantum Computing5, 1, Article 1 (Dec. 2023), 35 pages. https://doi.org/10.1145/ 3624483

    2023

  32. [40]

    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, ...

    2021 doi

  33. [41]

    Matthias Liero, Alexander Mielke, and Giuseppe Savaré. 2018. Optimal entropy-transport problems and a new Hellinger–Kantorovich distance between positive measures.Inventiones mathematicae211, 3 (2018), 969–1117

    2018

  34. [42]

    2002.Lectures on the coupling method

    Torgny Lindvall. 2002.Lectures on the coupling method. Courier Corporation

    2002

  35. [43]

    2024.Optimal Transport on Quantum Structures

    Jan Maas, Simone Rademacher, Tamás Titkos, and Dániel Virosztek (Eds.). 2024.Optimal Transport on Quantum Structures. Bolyai Society Mathematical Studies, Vol. 29. Springer Nature Switzerland, Cham. https://doi.org/10.1007/ 978-3-031-50466-2

    2024

  36. [44]

    Rupak Majumdar and VR Sathiyanarayana. 2025. Sound and complete proof rules for probabilistic termination. Proceedings of the ACM on Programming Languages9, POPL (2025), 1871–1902

    2025

  37. [45]

    The mathlib Community. 2020. The lean mathematical library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs(New Orleans, LA, USA)(CPP 2020). Association for Computing Machinery, New York, NY, USA, 367–381. https://doi.org/10.1145/...

    2020

  38. [46]

    2005.Abstraction, Refinement and Proof for Probabilistic Systems

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

    2005 doi

  39. [47]

    Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. 2017. A new proof rule for almost-sure termination.Proceedings of the ACM on Programming Languages2, POPL (2017), 1–28

    2017

  40. [48]

    2024.Transition to post-quantum cryptography standards

    Dustin Moody, Ray Perlner, Andrew Regenscheid, Angela Robinson, and David Cooper. 2024.Transition to post-quantum cryptography standards. Technical Report. National Institute of Standards and Technology

    2024

  41. [49]

    2010.Quantum computation and quantum information

    Michael A Nielsen and Isaac L Chuang. 2010.Quantum computation and quantum information. Cambridge university press

    2010

  42. [50]

    Raphael Overbeck and Nicolas Sendrier. 2009. Code-based cryptography. InPost-quantum cryptography. Springer, 95–145

    2009

  43. [51]

    Chris Peikert. 2016. A Decade of Lattice Cryptography.Foundations and Trends®in Theoretical Computer Science10, 4 (2016), 283–424. https://doi.org/10.1561/0400000074

    2016 doi

  44. [52]

    Peter Selinger. 2004. Towards a quantum programming language.Mathematical Structures in Computer Science14, 4 (2004), 527–586. https://doi.org/10.1017/S0960129504004256

    2004 doi

  45. [53]

    Peter W Shor and John Preskill. 2000. Simple proof of security of the BB84 quantum key distribution protocol.Physical review letters85, 2 (2000), 441

    2000

  46. [54]

    Volker Strassen. 1965. The existence of probability measures with given marginals.The Annals of Mathematical Statistics36, 2 (1965), 423 – 439. https://doi.org/10.1214/aoms/1177700153

    1965

  47. [55]

    2000.Coupling, Stationarity, and Regeneration

    Hermann Thorisson. 2000.Coupling, Stationarity, and Regeneration. springer. , Vol. 1, No. 1, Article . Publication date: October 2025. 30 G. Barthe, M. Gao, J. K. A. Khan, M. Muis, I. Renison, K. Sakabe, M. Walter, Y. Xu, and L. Zhou

    2000

  48. [56]

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

    2019 doi

  49. [57]

    Dominique Unruh. 2020. Post-Quantum Verification of Fujisaki-Okamoto. InAdvances in Cryptology - ASIACRYPT 2020 - 26th International Conference on the Theory and Application of Cryptology and Information Security, Daejeon, South Korea, December 7-11, 2020, Proceedings, Part I ...

    2020 doi

  50. [58]

    2023.Introduction to quantum cryptography

    Thomas Vidick and Stephanie Wehner. 2023.Introduction to quantum cryptography. Cambridge University Press

    2023

  51. [59]

    2008.Optimal transport: Old and new

    Cédric Villani. 2008.Optimal transport: Old and new. springer

    2008

  52. [60]

    Stephen Wiesner. 1983. Conjugate coding.ACM Sigact News15, 1 (1983), 78–88

    1983

  53. [61]

    Yingte Xu, Li Zhou, and Gilles Barthe. 2025. D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation. InComputer Aided Verification, Ruzica Piskac and Zvonimir Rakamarić (Eds.). Springer Nature Switzerland, Cham, 53–76

    2025

  54. [62]

    Hongseok Yang. 2007. Relational separation logic.Theor. Comput. Sci.375, 1-3 (2007), 308–334. https://doi.org/10. 1016/J.TCS.2006.12.036

    2007

  55. [63]

    2016.Foundations of quantum programming

    Mingsheng Ying. 2016.Foundations of quantum programming. Morgan Kaufmann

    2016

  56. [64]

    Mark Zhandry. 2019. How to record quantum queries, and applications to quantum indifferentiability. InAdvances in Cryptology–CRYPTO 2019: 39th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 18–22, 2019, Proceedings, Part II 39. Springer, 239–268

    2019

  57. [65]

    Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. 2023. CoqQ: Foundational Verification of Quantum Programs.Proc. ACM Program. Lang.7, POPL (2023), 833–865. https://doi.org/10.1145/3571222

    2023 doi

  58. [66]

    Li Zhou, Shenggang Ying, Nengkun Yu, and Mingsheng Ying. 2020. Strassen’s theorem for quantum couplings. Theoretical Computer Science802 (2020), 67–76. https://doi.org/10.1016/j.tcs.2019.08.026

    2020 doi

  59. [67]

    weak duality

    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...

    2019

  60. [68]

    (1)Let𝐶be positive definite

    This concludes the proof of the lemma.□ Lemma B.5 (Schur complement).Consider a Hermitian block matrix 𝐻= 𝐴 𝐵 𝐵† 𝐶 . (1)Let𝐶be positive definite. Then𝐻⊒0if and only if𝐵𝐶 −1𝐵†⊑𝐴. (2)Let𝛾,𝛼>0be such that𝐴⊒𝛼𝐼,𝐶⊒𝛾𝐼, and∥𝐵∥ 2≤𝛾𝛼. Then𝐻⊒0. , Vol. 1, No. 1, Article . Publication date...

    2025

  61. [69]

    (∀𝑎1∈A′ 1),Δ ′ 2(𝑎2)≜ Δ2(𝑎2) tr(Δ 2|A′

  62. [70]

    Note that tr(Δ′ 1)=tr(Δ ′ 2)= 1

    (∀𝑎2∈A′ 2). Note that tr(Δ′ 1)=tr(Δ ′ 2)= 1. Let us also denote by 𝜙′ ≜𝜙| A′ 1×A′ 2 the restriction of 𝜙 of the assertion. BecauseA′ 1 andA′ 2 are finite, we know from Theorem B.3 that the corresponding optimization problems have the same value: opt(P′)≜inf Δ′:⟨Δ′ 1,Δ′ 2⟩ EΔ′[...

  63. [71]

    We claim that Δ is a coupling of Δ1 and Δ2

    Then we defineΔ∈S (A 1×A 2,H1⊗H2) by Δ(𝑎 1,𝑎 2)≜ tr(Δ 1|A′ 1)tr(Δ 2|A′ 2)Δ′(𝑎1,𝑎 2)if(𝑎 1,𝑎 2)∈A ′ 1×A′ 2, Δ1(𝑎1)⊗Δ 2(𝑎2)otherwise. We claim that Δ is a coupling of Δ1 and Δ2. By symmetry, we only need to prove that tr2(Δ)=Δ 1. Indeed, for all𝑎 1∈A 1\A′ 1, we have tr2(Δ)(𝑎 1)=...

    2025

  64. [72]

    By adding these two , Vol

    By symmetry, we also have EΔ2(𝜓2)≥E Δ′ 2(𝜓′ 2)− 2𝛿∥𝜙∥− 4 √ 𝛿∥𝜙∥ 2. By adding these two , Vol. 1, No. 1, Article . Publication date: October 2025. A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics 41 inequalities, and using t...

    2025

  65. [73]

    is a √ 𝛿-approximate maximizer. Thus Eq. (7) follows. By combining Eqs. (5) to (7), we find that opt(P)≤opt(P ′)+2𝛿∥𝜙∥=opt(D ′)+2𝛿∥𝜙∥≤opt(D)+ √ 𝛿+6𝛿∥𝜙∥+8 √ 𝛿∥𝜙∥ 2. This holds for all𝛿∈( 0, 1), so we obtain opt(P)≤opt( D). But we also know that opt(P)≥opt( D) from weak duality ...

    2020

Pith tools

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