pith. sign in

arxiv: 2507.13635 · v4 · submitted 2025-07-18 · 🪐 quant-ph · cs.LO· cs.PL

SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits

Nengkun Yu , Jens Palsberg , Thomas Reps This is my paper

Pith reviewed 2026-05-19 04:58 UTC · model grok-4.3

classification 🪐 quant-ph cs.LOcs.PL
keywords quantum circuitsformal verificationapproximate reasoningscalable logicGHZ statesquantum phase estimationnon-Clifford gateslocal reasoning
0
0 comments X

The pith

The SAQR-QC logic performs scalable approximate quantitative reasoning on quantum circuits by confining each step to a few qubits and bounding accumulated precision loss.

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

The paper presents SAQR-QC as a logic that reasons about quantum circuits without requiring exponential resources in the number of qubits. It deliberately accepts some loss of precision but equips the logic with a way to keep that loss from growing large across a sequence of steps. Every individual reasoning step operates locally on only a small number of qubits. This design is illustrated through verification of GHZ circuits that include non-Clifford gates and through analysis of quantum phase estimation. A reader would care because existing methods become impractical once circuits grow beyond a handful of qubits, leaving many quantum algorithms without formal guarantees.

Core claim

SAQR-QC supports scalable but approximate quantitative reasoning about quantum circuits. Some loss of precision is built into the logic. A mechanism helps keep the accumulated loss small during sequences of steps. Most importantly, every reasoning step is local and involves just a small number of qubits. The approach is demonstrated on GHZ circuits with non-Clifford gates and on quantum phase estimation, a core part of Shor's algorithm.

What carries the argument

The SAQR-QC logic, whose central features are local reasoning steps on small qubit groups together with an explicit mechanism that bounds total precision loss across the full circuit.

If this is right

  • Properties of GHZ states produced by circuits containing non-Clifford gates become verifiable without building full state representations.
  • Quantitative statements about the precision of quantum phase estimation can be established by composing a modest number of local steps.
  • Reasoning about other quantum algorithms that rely on similar circuit structures becomes feasible at scales where exponential methods fail.
  • Verification effort can be allocated to small qubit subsets while still obtaining circuit-wide guarantees, provided the precision bound holds.

Where Pith is reading between the lines

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

  • The same locality principle might apply to circuits that include classical control if the approximation mechanism can be extended to handle measurement outcomes.
  • Similar approximate logics could be developed for other quantum models such as measurement-based computation.
  • Empirical checks on progressively larger circuits would reveal the practical size at which accumulated error remains tolerable for typical properties of interest.

Load-bearing premise

Local steps that each involve only a small number of qubits can be composed across an entire circuit while the built-in approximation mechanism keeps total precision loss small enough to remain useful for verifying key properties.

What would settle it

Running SAQR-QC on a circuit with dozens of qubits and observing that the tracked precision loss exceeds the margin required to confirm a target property such as the presence of entanglement or the accuracy of a phase estimate.

Figures

Figures reproduced from arXiv: 2507.13635 by Jens Palsberg, Nengkun Yu, Thomas Reps.

Figure 1
Figure 1. Figure 1: CNOT circuit C Let us reason about circuit C using Equation (10). We choose (𝑠1, 𝑠2) = ({𝑞1}, {𝑞2}) and 𝑀B = |0⟩⟨0| ⊗ 𝐼 + 𝐼 ⊗ |0⟩⟨0|. 𝑈 † C ∑︁ 𝑖 𝐵𝑠𝑖 ⊗ 𝐼[𝑛]\𝑠𝑖 ! 𝑈C = |0⟩⟨0| ⊗ 𝐼 + |0⟩⟨0| ⊗ |0⟩⟨0| + |1⟩⟨1| ⊗ |1⟩⟨1|. We now show that there is no 𝐴1 ≥ 0 and 𝐴2 ≥ 0 that satisfies |0⟩⟨0| ⊗ 𝐼 + |0⟩⟨0| ⊗ |0⟩⟨0| + |1⟩⟨1| ⊗ |1⟩⟨1| = 𝐴1 ⊗ 𝐼 + 𝐼 ⊗ 𝐴2. (11) Proc. ACM Program. Lang., Vol. 1, No. CONF, Article 1. Publica… view at source ↗
Figure 2
Figure 2. Figure 2: Inference rules for program constructs in [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: GHZ circuit with one-qubit unitaries 𝑈𝑖 . We select the following domain ({1, 2}, {2, 3}, · · · , {𝑛 − 1, 𝑛}). STEP 1. We first select the precondition to be {A |P} where A = (𝐴1,2, 𝐴2,3, · · · , 𝐴𝑛−1,𝑛) = (| + +⟩⟨+ + |, | + +⟩⟨+ + |, · · · , | + +⟩⟨+ + |) P = (𝑃1,2, 𝑃2,3, · · · , 𝑃𝑛−1,𝑛) = (|00⟩⟨00|, |00⟩⟨00|, · · · , |00⟩⟨00|). One can verify that the initial state |0 · · · 0⟩⟨0 · · · 0| ⊨ P. We now use … view at source ↗
Figure 4
Figure 4. Figure 4: Quantum Fourier transform. Swap gates at the end of the circuit that reverse the order of the qubits [PITH_FULL_IMAGE:figures/full_fig_p020_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Quantum Phase Estimation: 𝑈 |𝜓⟩ = 𝑒 𝑖𝜃 |𝜓⟩. We only consider the circuit without the measurements. We denote by C1 the segment of the program that precedes the application of the inverse Quantum Fourier Transform, QF T† . The QF T† operation can be decomposed into two parts: the initial sequence of swap gates that reverses the order of the qubits, and the subsequent controlled rotation gates that implement… view at source ↗
read the original abstract

Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Despite extensive research, existing verification techniques are insufficient -- even for quantum circuits, a deliberately restricted model that lacks classical control, but still underpins many current quantum algorithms. Many existing formal methods require exponential time and space to represent and manipulate (representations of) assertions and judgments, making them impractical for quantum circuits with many qubits. This paper presents a logic for reasoning in such settings, called SAQR-QC. The logic supports {S}calable but {A}pproximate {Q}uantitative {R}easoning about {Q}uantum {C}ircuits, whence the name. SAQR-QC has three characteristics: (i) some (deliberate) loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) most importantly, to make reasoning scalable, every reasoning step is local -- i.e., it involves just a small number of qubits. We demonstrate the effectiveness of SAQR-QC via two case studies: the verification of GHZ circuits involving non-Clifford gates, and the analysis of quantum phase estimation -- a core subroutine in Shor's factoring algorithm.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper introduces SAQR-QC, a logic for scalable but approximate quantitative reasoning about quantum circuits. It is characterized by built-in deliberate precision loss, a mechanism intended to keep accumulated precision loss small across reasoning steps, and locality of each reasoning step to a small number of qubits. The approach is demonstrated via case studies on GHZ state preparation circuits that include non-Clifford gates and on quantum phase estimation, a key subroutine in Shor's algorithm.

Significance. If the local approximate steps can be shown to compose while keeping total error bounded and useful (e.g., not degrading faster than the precision required by the target property), the logic would address a central scalability barrier in quantum-circuit verification. Existing methods often incur exponential cost in qubit number; a sound local-approximate framework could enable analysis of circuits whose size is currently out of reach.

major comments (2)
  1. [Abstract / QPE case study] Abstract and case-study description: the claim that a built-in mechanism keeps accumulated precision loss small is not accompanied by any derivation, theorem, or quantitative bound (e.g., total error scaling as O(1/poly(n)) rather than linearly with depth or qubit count). Without such a bound the composition argument for QPE remains unevaluated.
  2. [QPE case study] QPE case study: each local step may introduce controlled error, yet the manuscript supplies no explicit global error analysis showing that the final quantitative judgment remains tight enough to verify the key properties of phase estimation when the number of qubits grows. This is the load-bearing point for the scalability claim.
minor comments (1)
  1. [Logic definition] Notation for the approximation operators and the precision-control mechanism should be introduced with a small illustrative example before the full case studies.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We are grateful to the referee for their thorough review and constructive suggestions. The comments correctly identify that the manuscript lacks a formal bound on accumulated precision loss and a global error analysis for the QPE case study. We respond to these points below and commit to revisions that address the concerns while preserving the core contributions of the logic.

read point-by-point responses

  1. Referee: [Abstract / QPE case study] Abstract and case-study description: the claim that a built-in mechanism keeps accumulated precision loss small is not accompanied by any derivation, theorem, or quantitative bound (e.g., total error scaling as O(1/poly(n)) rather than linearly with depth or qubit count). Without such a bound the composition argument for QPE remains unevaluated.

    Authors: We thank the referee for highlighting this gap. SAQR-QC is designed with local rules that deliberately restrict approximation to a small number of qubits per step, which in principle limits error propagation. However, the manuscript provides no formal theorem or derivation establishing a quantitative bound on total accumulated error (such as O(1/poly(n)) scaling). The case studies illustrate practical use but do not constitute a general composition result. We will revise the abstract and QPE section to state this limitation explicitly and add a discussion of how locality may help bound error growth. revision: yes

  2. Referee: [QPE case study] QPE case study: each local step may introduce controlled error, yet the manuscript supplies no explicit global error analysis showing that the final quantitative judgment remains tight enough to verify the key properties of phase estimation when the number of qubits grows. This is the load-bearing point for the scalability claim.

    Authors: We agree that the QPE case study applies the local rules but does not include an explicit global error propagation analysis demonstrating that the final approximate judgment remains sufficiently tight as qubit count increases. The presented results show that the logic can be applied step-by-step to the circuit, yet a full accounting of how controlled local errors compose across the entire depth is absent. This point is indeed central to the scalability claim. In revision we will add a preliminary global error analysis for the QPE example, examining error accumulation over the sequence of controlled rotations and discussing the tightness of the resulting quantitative judgments. revision: yes

Circularity Check

0 steps flagged

No circularity: SAQR-QC introduces independent local approximate reasoning mechanisms grounded in standard quantum circuit semantics

full rationale

The paper defines SAQR-QC as a new logic with three explicit characteristics (deliberate precision loss, accumulation control, and locality to small qubit subsets) and demonstrates it via case studies on GHZ and QPE circuits. No load-bearing step reduces by construction to fitted inputs, self-definitions, or self-citation chains; the composition of local steps with bounded error is presented as a designed property of the logic rather than a tautology. The derivation remains self-contained against external quantum circuit models without requiring the target results as assumptions.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The approach rests on standard assumptions about quantum circuit structure and the feasibility of controlling approximation errors through local operations; no free parameters or invented physical entities are described.

axioms (2)
  • domain assumption Quantum circuits admit local reasoning steps on small subsets of qubits that can be composed to analyze global properties.
    Invoked to justify scalability via locality.
  • domain assumption Approximation errors can be bounded and kept small across sequences of reasoning steps.
    Central to the claim of controlled precision loss.
invented entities (1)
  • SAQR-QC logic no independent evidence
    purpose: Framework for scalable approximate quantitative reasoning about quantum circuits
    Newly defined logic with three explicit characteristics.

pith-pipeline@v0.9.0 · 5775 in / 1280 out tokens · 48769 ms · 2026-05-19T04:58:28.687455+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

  • IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel echoes
    ?
    echoes

    ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

    SAQR-QC has three characteristics: (i) some (deliberate) loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) most importantly, to make reasoning scalable, every reasoning step is local—i.e., it involves just a small number of qubits.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 2 Pith papers

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

  1. A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)

    cs.LO 2026-05 unverdicted novelty 8.0

    An extended set-based specification language translates to compact automata in linear time in the number of qubits, enabling fully automatic Hoare-style verification of quantum programs at larger scales.

  2. Hybrid Path-Sums for Hybrid Quantum Programs

    cs.PL 2026-04 unverdicted novelty 7.0

    Hybrid Path-Sums offer a new symbolic framework with rewriting rules and assertions to represent, simplify, and verify properties of hybrid quantum-classical programs.

Reference graph

Works this paper leans on

45 extracted references · 45 canonical work pages · cited by 2 Pith papers · 1 internal anchor

  1. [1]

    Physical Review A 70(5) (Nov 2004)

    Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Physical Review A 70(5) (Nov 2004). https://doi.org/10.1103/physreva.70.052328, http://dx.doi.org/10.1103/PhysRevA.70.052328

    work page doi:10.1103/physreva.70.052328 2004

  2. [2]

    Abdulla, P.A.: A symbolic approach to verifying quantum systems. Commun. ACM 68(6), 84 (Jun 2025). https://doi.org/10.1145/3725725, https://doi.org/10.1145/3725725

    work page doi:10.1145/3725725 2025

  3. [3]

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

    work page doi:10.1145/3704873 2025

  4. [4]

    Science309(5741), 1704–1707 (2005),https: //www.science.org/doi/abs/10.1126/science.1113479

    Aspuru-Guzik, A., Dutoi, A.D., Love, P.J., Head-Gordon, M.: Simulated quantum computation of molecular energies. Science 309(5741), 1704–1707 (2005). https://doi.org/10.1126/science.1113479

    work page doi:10.1126/science.1113479 2005

  5. [5]

    Barthe, G., Hsu, J., Ying, M., Yu, N., Zhou, L.: Relational proofs for quantum programs. Proc. ACM Program. Lang. 4(POPL) (2020)

    work page 2020

  6. [6]

    In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P

    Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures. Lecture Notes in Computer ...

    work page doi:10.1007/11804192_6 2005

  7. [7]

    Quantum 7, 1185 (Nov 2023)

    Bichsel, B., Paradis, A., Baader, M., Vechev, M.: Abstraqt: Analysis of quantum circuits via abstract stabilizer simulation. Quantum 7, 1185 (Nov 2023). https://doi.org/10.22331/q-2023-11-20-1185, http://dx.doi.org/10.22331/q-2023-11-20-1185

    work page doi:10.22331/q-2023-11-20-1185 2023

  8. [8]

    Annals of Mathematics 37(4), 823–843 (1936)

    Birkhoff, G., Von Neumann, J.: The logic of quantum mechanics. Annals of Mathematics 37(4), 823–843 (1936)

    work page 1936

  9. [9]

    In: Cytron, R., Gupta, R

    Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Cytron, R., Gupta, R. (eds.) Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, San Diego, California, USA, June 9-11, 2003. pp. 196–207. ACM (2003)...

    work page doi:10.1145/781131.781153 2003

  10. [10]

    Electronic Notes in Theoretical Computer Science 158, 19–39 (2006)

    Chadha, R., Mateus, P., Sernadas, A.: Reasoning about imperative quantum programs. Electronic Notes in Theoretical Computer Science 158, 19–39 (2006)

    work page 2006

  11. [11]

    Chen, Y., Chung, K., Lengál, O., Lin, J., Tsai, W., Yen, D.: An automata-based framework for verification and bug hunting in quantum circuits. Proc. ACM Program. Lang. 7(PLDI), 1218–1243 (2023). https://doi.org/10.1145/3591270, https://doi.org/10.1145/3591270

    work page doi:10.1145/3591270 2023

  12. [12]

    CACM 68(6)

    Chen, Y.F., Chung, K.M., Lengál, O., Lin, J.A., Tsai, W.L., Yen, D.D.: An automata-based framework for verification and bug hunting in quantum circuits. CACM 68(6)

    work page

  13. [13]

    In: Dershowitz, N

    Cousot, P.: Verification by abstract interpretation. In: Dershowitz, N. (ed.) Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. Lecture Notes in Computer Science, vol. 2772, pp. 243–268. Springer (2003). https://doi.org/10.1007/978-3-540-39910-0_11, https://doi.org/10.1007/978-3-540-39910-0_11

    work page doi:10.1007/978-3-540-39910-0_11 2003

  14. [14]

    In: Graham, R.M., Harrison, M.A., Sethi, R

    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977. pp. 238–252. ACM (1977)....

    work page doi:10.1145/512950.512973 1977

  15. [15]

    In: Aho, A.V., Zilles, S.N., Rosen, B.K

    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979. pp. 269–282. ACM Press (1979). https://doi.org/10.1145/567752.567778, https: //doi.org/10.1145/567752.567778

    work page doi:10.1145/567752.567778 1979

  16. [16]

    Mathematical Structures in Computer Science16(3), 429–451 (2006)

    D’Hondt, E., Panangaden, P.: Quantum weakest preconditions. Mathematical Structures in Computer Science16(3), 429–451 (2006)

    work page 2006

  17. [17]

    In: Hermanns, H., Palsberg, J

    Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25...

    work page doi:10.1007/11691372_19 2006

  18. [18]

    Farhi, E., Goldstone, J., Gutmann, S.: A quantum approximate optimization algorithm (2014), https://arxiv.org/abs/1411. 4028

    work page 2014

  19. [19]

    Feng, Y., Ying, M.: Quantum hoare logic with classical variables (2021)

    work page 2021

  20. [20]

    Physical Review Letters 103(15), 150502 (2009)

    Harrow, A.W., Hassidim, A., Lloyd, S.: Quantum algorithm for linear systems of equations. Physical Review Letters 103(15), 150502 (2009)

    work page 2009

  21. [21]

    Hietala, K., Rand, R., Hung, S.H., Wu, X., Hicks, M.: A verified optimizer for quantum circuits. No. POPL’2021 (2021)

    work page 2021

  22. [22]

    Hung, S.H., Hietala, K., Zhu, S., Ying, M., Hicks, M., Wu, X.: Quantitative robustness analysis of quantum programs. Proc. ACM Program. Lang. 3(POPL), 31:1–31:29 (2019) Proc. ACM Program. Lang., Vol. 1, No. CONF, Article 1. Publication date: January 2018. SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits 1:27

    work page 2019

  23. [23]

    In: Datta, A

    Kakutani, Y.: A logic for formal verification of quantum programs. In: Datta, A. (ed.) Advances in Computer Science - ASIAN 2009. Information Security and Privacy. pp. 79–93. Springer Berlin Heidelberg, Berlin, Heidelberg (2009)

    work page 2009

  24. [24]

    Quantum measurements and the Abelian Stabilizer Problem

    Kitaev, A.Y.: Quantum measurements and the abelian stabilizer problem. arXiv:quant-ph/9511026 (1995)

    work page internal anchor Pith review Pith/arXiv arXiv 1995

  25. [25]

    Le, X.B., Lin, S.W., Sun, J., Sanan, D.: A quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic. Proc. ACM Program. Lang. 6(POPL) (jan 2022). https://doi.org/10.1145/3498697, https://doi.org/10.1145/3498697

    work page doi:10.1145/3498697 2022

  26. [26]

    In: Proceedings of the 48th International Colloquium on Automata, Languages, and Programming

    Li, Y., Unruh, D.: Quantum relational hoare logic with expectations. In: Proceedings of the 48th International Colloquium on Automata, Languages, and Programming. pp. 136:1–136:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

    work page 2021

  27. [27]

    Cambridge University Press, New York, NY, USA, 10th edn

    Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, New York, NY, USA, 10th edn. (2011)

    work page 2011

  28. [28]

    Bulletin of Symbolic Logic 5(2), 215–244 (1999)

    O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999). https://doi.org/10.2307/421090

    work page doi:10.2307/421090 1999

  29. [29]

    https://doi.org/10.48550/ARXIV.2204.07112, https://arxiv.org/abs/2204.07112

    Peng, Y., Hietala, K., Tao, R., Li, L., Rand, R., Hicks, M., Wu, X.: A formally certified end-to-end implementation of shor’s factorization algorithm (2022). https://doi.org/10.48550/ARXIV.2204.07112, https://arxiv.org/abs/2204.07112

    work page doi:10.48550/arxiv.2204.07112 2022

  30. [30]

    Rand, R.: Verification logics for quantum programs (2019)

    work page 2019

  31. [31]

    In: Steffen, B., Levi, G

    Reps, T.W., Sagiv, S., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) Ver- ification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2937, pp. 252–266. Springer (2004). https://doi.o...

    work page doi:10.1007/978-3-540-24622-0_21 2004

  32. [32]

    In: Jobstmann, B., Leino, K.R.M

    Reps, T.W., Thakur, A.V.: Automating abstract interpretation. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. Lecture Notes in Computer Science, vol. 9583, pp. 3–40. Springer (2016). https://doi.org/10.1...

    work page doi:10.1007/978-3-662-49122-5_1 2016

  33. [33]

    In: Ferrante, J., McKinley, K.S

    Scherpelz, E.R., Lerner, S., Chambers, C.: Automatic inference of optimizer flow functions from semantic mean- ings. In: Ferrante, J., McKinley, K.S. (eds.) Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007. pp. 135–145. ACM (2007). https://doi.org/10.1145/1250734...

    work page doi:10.1145/1250734.1250750 2007

  34. [34]

    SIAM Journal on Computing 26(5), 1484–1509 (1997)

    Shor, P.: Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM Journal on Computing 26(5), 1484–1509 (1997)

    work page 1997

  35. [35]

    In: Pro- ceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

    Tao, R., Shi, Y., Yao, J., Hui, J., Chong, F.T., Gu, R.: Gleipnir: Toward practical error analysis for quantum programs. In: Pro- ceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. p. 48–64. PLDI 2021, Association for Computing Machinery, New York, NY, USA (2021)

    work page 2021

  36. [36]

    In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

    Tao, R., Shi, Y., Yao, J., Li, X., Javadi-Abhari, A., Cross, A.W., Chong, F.T., Gu, R.: Giallar: push-button verification for the qiskit quantum compiler. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. p. 641–656. PLDI 2022, Association for Computing Machinery, New York, NY, USA (2022). ...

    work page doi:10.1145/3519939.3523431 2022

  37. [37]

    Medaglia

    Thakur, A.V., Reps, T.W.: A method for symbolic computation of abstract operations. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Lecture Notes in Computer Science, vol. 7358, pp. 174–192. Springer (2012). https://doi.org/10.1007/978-3- 642-314...

    work page doi:10.1007/978-3- 2012

  38. [38]

    In: ACM/IEEE Symposium on Logic in Computer Science

    Unruh, D.: Quantum hoare logic with ghost variables. In: ACM/IEEE Symposium on Logic in Computer Science. LICS 2019 (2019)

    work page 2019

  39. [39]

    In: Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages

    Unruh, D.: Quantum relational hoare logic. In: Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages. POPL 2019, ACM, New York, NY, USA (2019)

    work page 2019

  40. [40]

    Wikipedia contributors: Gottesman–Knill theorem (2025), https://en.wikipedia.org/wiki/Gottesman%E2%80%93Knill_ theorem, accessed: 2025-01-29

    work page 2025

  41. [41]

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

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

    work page 2011

  42. [42]

    In: Proceedings of the 42th ACM SIGPLAN Conference on Programming Language Design and Implementation

    Yu, N., Palsberg, J.: Quantum abstract interpretation. In: Proceedings of the 42th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2021, Association for Computing Machinery, New York, NY, USA (2021)

    work page 2021

  43. [43]

    In: Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2021)

    Zhou, L., Barthe, G., Hsu, J., Ying, M., Yu, N.: A quantum interpretation of bunched logic for quantum separation logic. In: Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2021)

    work page 2021

  44. [44]

    Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science , articleno =

    Zhou, L., Barthe, G., Hsu, J., Ying, M., Yu, N.: A Quantum Interpretation of Bunched Logic for Quantum Separation Logic. Association for Computing Machinery, New York, NY, USA (2021), https://doi.org/10.1109/LICS52264.2021.9470673 Proc. ACM Program. Lang., Vol. 1, No. CONF, Article 1. Publication date: January 2018. 1:28 Nengkun Yu, Jens Palsberg, and Thomas Reps

    work page doi:10.1109/lics52264.2021.9470673 2021

  45. [45]

    In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

    Zhou, L., Yu, N., Ying, M.: An applied quantum hoare logic. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 1149–1162. PLDI 2019, ACM, New York, NY, USA (2019) Proc. ACM Program. Lang., Vol. 1, No. CONF, Article 1. Publication date: January 2018. SAQR-QC: A Logic for Scalable but Approximate Quanti...

    work page 2019