Pith. sign in

REVIEW 3 major objections 4 minor 90 references

Laws of Quantum Programming

T0 review · 3 major / 4 minor · reviewed 2026-08-11 · deepseek-v4-flash

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

Pith's one-line read The paper claims that quantum programming has a comprehensive, machine-checked lawbook: a unified set of algebraic laws for circuits, purely quantum programs, and hybrid programs, with all laws mechanically verified in Coq.

desk verdict A substantial, well-done systematic algebra for quantum programming with real Coq backing, but the 'all mechanically verified' claim outruns what the paper actually pins down. read the letter →

arxiv 2412.19463 v2 pith:DPDZJGFK submitted 2024-12-27 cs.PL

Mingsheng Ying , Li Zhou , Gilles Barthe This is my paper · ORCID
classification cs.PL MSC 68Q6081P68
keywords quantumprogrammingalgebraiclawsofcircuitsif-statementwhile-loopsnormalformsprogramtransformationmachine-checkedverificationinCoq
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 tries to establish a comprehensive set of algebraic laws for quantum programs, arranged in three layers: quantum circuits, purely quantum programs without classical variables, and classical-quantum hybrid programs. These laws generalize the classical laws of programming, characterizing how quantum if-statements, sequential composition, loops, recursion, and nondeterministic choice behave algebraically. The paper further proves two normal-form theorems, a fixpoint characterization of quantum while-loops, and a loop-based realization of tail recursion, and it derives the principle of deferred measurements from the laws. Every law presented is formally verified in the Coq proof assistant, so if the formalization is sound, the laws can be used as machine-checked justification for quantum program transformation and optimization.

What carries the argument

The central object is the quantum if-statement, a quantum multiplexor that generalizes the classical conditional, together with measurement-guarded if and while constructs at the program layer. The mechanism carrying the argument is the denotational semantics in which programs are quantum operations on density operators under the Löwner order, making the space of quantum operations a complete partial order in which loops and recursion are computed as least upper bounds. All laws are proved against this semantics and then checked in the Coq proof assistant.

What would settle it

Run the Coq development linked in Section 10 with the stated dependencies: if any law proved in Sections 4 through 9 fails to type-check, or if the formalized semantics of the quantum while-language contradicts Proposition 3.1, the central claim of mechanical verification fails. A semantic falsifier would be a regular quantum circuit whose Coq-computed normal form is denotationally different from the original circuit.

Watch

Extended reading notes

Core claim

The central claim is that quantum programming admits a lawful algebraic foundation in the same spirit as classical programming. Programs are given a denotational semantics in which they denote quantum operations on density operators, ordered by the Löwner order, so that loops and recursive programs are least upper bounds of their finite approximants. Against this semantics the paper proves laws for quantum circuits, such as distributivity of sequential composition over quantum if-statements, and laws for purely quantum programs, such as initialization laws, if-statement laws subject to measurement conditions, and loop laws. It also proves that every regular quantum circuit is equivalent to a sequential composition of flat quantum if-statements, that every finite quantum program is equivalent to a single measurement-guarded if-statement whose branches are circuits or abort, and that tail-recursive quantum programs with classical control flow are equivalent to a loop followed by the return code. The principle of deferred measurements is then derived as a formal consequence of these laws.

Load-bearing premise

The load-bearing premise is that the Coq formalization of Hilbert spaces, density operators, and quantum operations faithfully captures the intended quantum-mechanical semantics, because every law inherits its correctness from that model.

Editorial extensions

If this is right

  • Every regular quantum circuit can be rewritten into a sequential composition of flat quantum if-statements, which gives a concrete route to equivalence checking by comparing normal forms.
  • Every finite quantum program without loops or recursion can be normalized to a single if-statement whose branches are circuits or abort, offering a structured target for compilation and optimization.
  • Tail-recursive quantum programs can be implemented as loops, so classical compilation strategies for tail recursion transfer to quantum programs with classical control flow.
  • The formal derivation of deferred measurements means that dynamic quantum circuits can be mechanically transformed into a circuit followed by a final measurement.
  • Because all laws are machine-checked, a compiler or optimizer that applies them as rewrite rules is sound by construction.

Reading between the lines

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

  • The law-based rewriting used to prove the quantum error-correction example could be packaged as a certified optimization pass: applying the laws in reverse lowers a high-level quantum program into a normalized circuit with Coq supplying the correctness certificate.
  • The explicit side conditions on measurements, such as commutativity and logical strength, suggest that an automated tactic library could decide these conditions and make the framework usable beyond interactive proof.
  • If the Coq artifact is pinned to a specific commit and built reproducibly, this lawbook could serve as a shared substrate for verifying quantum compilers; the paper itself does not yet provide that reproducibility guarantee.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

Summary. The paper develops an algebraic theory of quantum programming organized in three layers: quantum circuits, purely quantum programs, and classical-quantum hybrid programs. It states and proves laws for quantum if-statements, initialization, measurement-based if-statements, sequential composition, loops, recursion, nondeterministic choice, and refinement, together with two normal form theorems (for circuits and for finite programs), a loop-based realization of tail recursion, and a formal derivation of the principle of deferred measurements. The paper claims that all of these laws are mechanically verified in the Coq proof assistant via the CoqQ framework, and it illustrates the laws on a quantum error-correction program, quantum teleportation, circuit optimization, and a quantum random walk.

Significance. The paper's ambition is appropriate and the mathematical development is largely transparent: the laws are proved from the denotational semantics rather than assumed, so there is no circularity in later deriving the deferred-measurement principle from them. The worked QEC and teleportation derivations are valuable demonstrations that the laws compose into substantial program transformations, and the two normal-form theorems, if completed, give a principled path toward equivalence checking and compilation. The explicit statement of Conjecture C.1 is an honest delimitation of the theory. The principal value is, however, conditional on the Coq artifact: if the formalization is faithful and matches the paper's statements, then the paper delivers machine-checked algebraic laws for a significant fragment of quantum programming, which would be a strong contribution to the journal's readership.

major comments (3)
  1. [Section 10, Abstract] The headline claim that 'all of these laws are mechanically verified' is not auditable from the manuscript. The Coq development is referenced by a URL only; no commit hash, Coq/MathComp/MathComp-Analysis versions, build instructions, or a mapping from theorems in Sections 4 through 9 to Coq theorem names are supplied. In addition, the paper states laws for arbitrary Hilbert spaces (Section 3; Example 4.1 uses an infinite-dimensional position space), whereas CoqQ, as published, is a finite-dimensional matrix formalization. Unless the Coq statements are explicitly restricted to finite-dimensional systems and the paper's claims are narrowed accordingly, the mechanical-verification claim cannot be checked to match the paper's statements. This is load-bearing because the verification claim is a central contribution; please pin the artifact and state the exact formalized scope.
  2. [Theorem 5.1, Section 5.5] The induction proof of the normal form theorem covers skip, abort, sequential composition, and if-statements, but the syntax (10) also contains initialization q:=|ψ> and quantum circuits C, both of which are within the theorem's scope as finite, purely quantum programs. No proof is given that either can be brought to the normal form (16). The cases are probably routine (a circuit can be placed in a trivial if-statement, and an initialization can be written as a measurement followed by state-preparation unitaries), but the omitted state-preparation unitaries also require an assumption about the available gate set U. Please add the base cases and the needed hypothesis on U.
  3. [Theorem 9.1 and Lemma 9.1] The deferred-measurement derivation silently assumes that the unitary operators U_M (Lemma 9.1) and U_|φ> (Appendix B, Case 2) can appear in the circuit C∈QC. But QC contains only unitary matrix constants from the fixed set U. The theorem states no hypothesis that U contains these unitaries; without such an assumption the asserted existence of C is not guaranteed for arbitrary finite programs (e.g., initialization to a state not preparable by the available gates). Please add an explicit closure condition on U or rephrase the theorem over an extended gate set.
minor comments (4)
  1. [Theorem 4.1 proof] The proof cites 'Proposition 4.1(14)'; the intended reference is Eq. (14), the Splitting law, not a proposition clause.
  2. [Propositions 4.1 and 4.2; Example 4.3] The headings contain typos: 'qantum if-statement', 'seqential composition', and 'Eqivalent checking' should be corrected.
  3. [Section 10] A table listing each law of Sections 4 through 8 with its corresponding Coq identifier would make the machine-checked claim substantially easier to verify than a URL alone.
  4. [Appendix C] Conjecture C.1 is disclosed as unproved; because the paper advertises a 'comprehensive' set of laws, please state in the main text that loop refinement is conjectural and not part of the mechanized verification.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the laws are proved from the denotational semantics, and the Coq formalization is a machine-checked verification rather than a fitted input.

full rationale

The paper's derivation chain starts from a fixed denotational semantics (Definition 3.3 and Proposition 3.1) and proves the laws from that semantics in Appendices A and B. The laws are not assumed as axioms: Proposition 4.2 is justified by expanding the circuit semantics, Proposition 5.2 by applying Proposition 3.1(5), Proposition 6.3 by manipulating the infinite-sum semantics of loops, and Theorem 6.1 by algebraic manipulation of the same infinite sum together with continuity proved in [77]. The normal-form theorems construct a normal form and then prove semantic equivalence to the original program; they are not definitions of equivalence in disguise. Theorem 9.1 is derived inductively from the earlier laws, with the key step using Proposition 5.5, rather than restating Lemma 9.1 or the deferred-measurement principle. The Coq verification claim in Section 10 relies on CoqQ [85] and on CPO/continuity facts cited to [77]; these are prior published or machine-checked results with stated assumptions that do not include the target laws, so under the review rules they count as independent support rather than load-bearing self-citation. The absence of a commit hash and build instructions for the Coq development is an auditability and reproducibility limitation, not a circularity, because it concerns whether the artifact can be checked, not whether the paper's derivations reduce to their own inputs. Conjecture C.1 is openly stated as unproved and therefore cannot be a circular step. Overall, the derivation chain is self-contained against the denotational semantics and shows no fitted-input, self-definitional, or renamed-ansatz circularity.

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

No free parameters are fitted and no new physical entities are postulated. The paper's contribution is a set of laws derived from existing denotational semantics; its novelty is in the algebraic laws, normal forms, tail-recursion theorem, and Coq formalization, not in new physical postulates.

assumptions (3)
  • domain assumption Quantum operations on a finite-dimensional Hilbert space form a CPO under the Löwner order, and the semantics of every quantum program is a continuous function on this CPO.
    Assumed from Ying's book [77] and used in Propositions 3.1(6), 6.1, 6.2, and Theorem 6.1 for fixpoint characterization of loops and recursion.
  • standard math Any quantum measurement can be implemented by a unitary on a larger system followed by a projective measurement on an ancilla.
    Used in Lemma 9.1 and Theorem 9.1 for the derivation of the deferred measurements principle; the paper cites Nielsen and Chuang [48].
  • domain assumption The semantics of nondeterministic quantum programs is given by sets of quantum operations, with refinement defined via convex hull and topological closure.
    Adopted from Feng and Xu [24] and Feng, Zhou, and Xu [25]; underpins all nondeterminism and refinement laws in Sections 7 and 8.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Laws of Quantum Programming." pith.science (2026). https://pith.science/paper/DPDZJGFK

@misc{pith2026241219463,
  author       = {Pith},
  title        = {Pith review of: Laws of Quantum Programming},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DPDZJGFK}},
  note         = {Machine review of arXiv:2412.19463}
}
read the original abstract

In this paper, we investigate the fundamental laws of quantum programming. We extend a comprehensive set of Hoare et al.'s basic laws of classical programming to the quantum setting. These laws characterise the algebraic properties of quantum programs, such as the distributivity of sequential composition over (quantum) if-statements and the unfolding of nested (quantum) if-statements. At the same time, we clarify some subtle differences between certain laws of classical programming and their quantum counterparts. Additionally, we derive a fixpoint characterisation of quantum while-loops and a loop-based realisation of tail recursion in quantum programming. Furthermore, we establish two normal form theorems: one for quantum circuits and one for finite quantum programs. The theory in which these laws are established is formalised in the Coq proof assistant, and all of these laws are mechanically verified. As an application case of our laws, we present a formal derivation of the principle of deferred measurements in dynamic quantum circuits. We expect that these laws can be utilised in correctness-preserving transformation, compilation, and automatic code optimisation in quantum programming. In particular, because these laws are formally verified in Coq, they can be confidently applied in quantum program development.

Figures

Figures reproduced from arXiv: 2412.19463 by the authors.

Figure 1
Figure 1. Three-Layer Framework for Quantum Programming. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Laws of Classical Programming. In law (If-6), [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. A convenient presentation of the ZX-calculus rules from [ [PITH_FULL_IMAGE:figures/full_fig_p050_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

90 extracted references · 32 canonical work pages

  1. [1]

    Ali J Abhari, Arvin Faruque, Mohammad J Dousti, Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, and Fred Chong. 2012. Scaffold: Quantum programming language . Technical Report. Princeton University

    2012

  2. [2]

    Altenkirch and J

    T. Altenkirch and J. Grattage. 2005. A functional quantum programming language. In 20th Annual IEEE Symposium on Logic in Computer Science (LICS’ 05) . 249–258. https://doi.org/10.1109/LICS.2005.1

    doi:10.1109/lics.2005.1 2005

  3. [3]

    Matthew Amy. 2018. Towards Large-scale Functional Verification of Universal Quantum Circuits. In Proceedings 15th International Conference on Quantum Physics and Logic, QPL 2018, Halifax, Canada, 3-7th June 2018 (EPTCS, Vol. 287) , Peter Selinger and Giulio Chiribella (Eds.). 1–21. https://doi.org/10.4204/EPTCS.287.1 ACM Trans. Softw. Eng. Methodol., Vol....

    doi:10.4204/eptcs.287.1 2018

  4. [4]

    Pablo Arrighi, Alejandro Díaz-Caro, and Benoît Valiron. 2017. The vectorial𝜆-calculus. Information and Computation 254 (2017), 105–139. https://doi.org/10.1016/j.ic.2017.04.001

    work page doi:10.1016/j.ic.2017.04.001 2017

  5. [6]

    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. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (Virtual Event, Republic of Korea) (CCS ’21). Association for Computing Machinery,...

    arXiv 2021

  6. [7]

    Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2014. EasyCrypt: A Tutorial. Springer International Publishing, Cham, 146–166. https://doi.org/10.1007/978-3-319-10082-1_6

    work page doi:10.1007/978-3-319-10082-1_6 2014

  7. [8]

    Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2010. Programming Language Techniques for Cryptographic Proofs. In Interactive Theorem Proving, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 115–130

    2010

  8. [9]

    Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. 2020. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (London, UK) (PLDI 2020). Association for Computing Machinery, New York, NY, USA, 286–300. https:/...

    arXiv 2020

Show all 90 references
  1. [10]

    François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages . Wroclaw, Poland, 53–64. https://inria.hal.science/hal-00790310

    2011

  2. [11]

    Anthony Bordg, Hanna Lachnitt, and Yijun He. 2020. Isabelle marries dirac: A library for quantum computation and quantum information. Archive of Formal Proofs (2020)

    2020

  3. [12]

    Anthony Bordg, Hanna Lachnitt, and Yijun He. 2021. Certified Quantum Computation in Isabelle/HOL. Journal of Automated Reasoning 65, 5 (01 June 2021), 691–709. https://doi.org/10.1007/s10817-020-09584-7

    2021 doi

  4. [13]

    Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Soulé, Robert Rand, and Patrick Eugster. 2024. An Algebraic Language for Specifying Quantum Networks. Proc. ACM Program. Lang. 8, PLDI, Article 200 (jun 2024), 23 pages. https://doi.org/10.1145/3656430

    2024 doi

  5. [14]

    Lukas Burgholzer and Robert Wille. 2021. Advanced Equivalence Checking for Quantum Circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 40, 9 (2021), 1810–1824. https://doi.org/10.1109/TCAD. 2020.3032630

    2021

  6. [15]

    Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, and Benoît Valiron. 2021. An Automated Deductive Verification Framework for Circuit-building Quantum Programs. In Programming Languages and Systems , Nobuko Yoshida (Ed.). Springer International Publishi...

    2021 doi

  7. [16]

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

    2023

  8. [17]

    Bob Coecke and Ross Duncan. 2011. Interacting quantum observables: categorical algebra and diagrammatics. New Journal of Physics 13, 4 (apr 2011), 043016. https://doi.org/10.1088/1367-2630/13/4/043016

    2011 doi

  9. [18]

    A. D. Córcoles, Maika Takita, Ken Inoue, Scott Lekuch, Zlatko K. Minev, Jerry M. Chow, and Jay M. Gambetta. 2021. Exploiting Dynamic Quantum Circuits in a Quantum Algorithm with Superconducting Qubits. Phys. Rev. Lett. 127 (Aug 2021), 100501. Issue 10. https://doi.org/10.1103/...

    2021 doi

  10. [19]

    Cirq Developers. 2025. Cirq. https://doi.org/10.5281/zenodo.15191735

    2025 doi

  11. [20]

    Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, and Benoît Valiron. 2019. Realizability in the Unitary Sphere. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. 1–13. https://doi.org/10.1109/LICS.2019.8785834

    2019

  12. [21]

    Dijkstra

    Edsger W. Dijkstra. 1975. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 8 (aug 1975), 453–457. https://doi.org/10.1145/360933.360975

    1975

  13. [22]

    Edsger Wybe Dijkstra, Edsger Wybe Dijkstra, Edsger Wybe Dijkstra, Etats-Unis Informaticien, and Edsger Wybe Dijkstra. 1976. A discipline of programming . Vol. 613924118. prentice-hall Englewood Cliffs

    1976

  14. [23]

    Ross Duncan, Aleks Kissinger, Simon Perdrix, and John van de Wetering. 2020. Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus. Quantum 4 (June 2020), 279. https://doi.org/10.22331/q-2020-06-04-279

    2020 doi

  15. [24]

    Yuan Feng and Yingte Xu. 2023. Verification of Nondeterministic Quantum Programs. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3 (ASPLOS 2023). Association for Computing Machinery, New ...

    2023

  16. [25]

    Yuan Feng, Li Zhou, and Yingte Xu. 2023. Refinement calculus of quantum programs with projective assertions. arXiv:2311.14215 [cs.LO]

    2023 arXiv

  17. [26]

    Gawron, J

    P. Gawron, J. Klamka, J. Miszczak, and R. Winiarczyk. 2010. Extending scientific computing system with structural quantum programming capabilities. online. Bulletin of the Polish Academy of Sciences Technical Sciences 58, No 1 (2010), 77–88. https://doi.org/10.2478/v10175-010-0008-4

    2010 doi

  18. [27]

    Gerdt and Alexander N

    Vladimir P. Gerdt and Alexander N. Prokopenya. 2013. Simulation of Quantum Error Correction with Mathematica. In Computer Algebra in Scientific Computing, Vladimir P. Gerdt, Wolfram Koepf, Ernst W. Mayr, and Evgenii V. Vorozhtsov (Eds.). Springer International Publishing, Cham...

    2013

  19. [28]

    Green, Peter LeFanu Lumsdaine, Neil J

    Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. 2013. Quipper: a scalable quantum programming language. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (Seattle, Washington, USA) ...

    2013

  20. [29]

    Jingzhe Guo, Huazhe Lou, Jintao Yu, Riling Li, Wang Fang, Junyi Liu, Peixun Long, Shenggang Ying, and Mingsheng Ying. 2023. isQ: An Integrated Software Stack for Quantum Programming. IEEE Transactions on Quantum Engineering 4 (2023), 1–16. https://doi.org/10.1109/TQE.2023.3275868

    2023

  21. [30]

    Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks. 2021. Proving Quantum Programs Correct. In 12th International Conference on Interactive Theorem Proving (ITP 2021) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 193), Liron Cohen and Ceza...

    2021 doi

  22. [31]

    Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. 2021. A verified optimizer for Quantum circuits. 5, POPL, Article 37 (jan 2021), 29 pages. https://doi.org/10.1145/3434318

    2021 doi

  23. [32]

    C. A. R. Hoare, I. J. Hayes, He Jifeng, C. C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sorensen, J. M. Spivey, and B. A. Sufrin. 1987. Laws of programming. Commun. ACM 30, 8 (aug 1987), 672–686. https://doi.org/10.1145/27651.27653

    1987

  24. [33]

    C. A. R. Hoare, He Jifeng, and A. Sampaio. 1993. Normal form approach to compiler design. Acta Informatica 30, 8 (01 Aug 1993), 701–739. https://doi.org/10.1007/BF01191809

    1993 doi

  25. [34]

    Wood, Jake Lishman, Julien Gacon, Simon Martiel, Paul D

    Ali Javadi-Abhari, Matthew Treinish, Kevin Krsulich, Christopher J. Wood, Jake Lishman, Julien Gacon, Simon Martiel, Paul D. Nation, Lev S. Bishop, Andrew W. Cross, Blake R. Johnson, and Jay M. Gambetta. 2024. Quantum computing with Qiskit. arXiv:2405.08810 [quant-ph] https://...

    2024 arXiv

  26. [35]

    Seidel, and A

    He Jifeng, K. Seidel, and A. McIver. 1997. Probabilistic models for the guarded command language. Science of Computer Programming 28, 2 (1997), 171–192. https://doi.org/10.1016/S0167-6423(96)00019-6 Formal Specifications: Foundations, Methods, Tools and Applications

    1997 doi

  27. [36]

    Aleks Kissinger and John van de Wetering. 2019. PyZX: Large Scale Automated Diagrammatic Reasoning. InProceedings 16th International Conference on Quantum Physics and Logic, QPL 2019, Chapman University, Orange, CA, USA, June 10-14, 2019 (EPTCS, Vol. 318) , Bob Coecke and Matt...

    2019 doi

  28. [37]

    Aleks Kissinger and John van de Wetering. 2024. Picturing Quantum Software: An Introduction to the ZX-Calculus and Quantum Compilation. Preprint

    2024

  29. [38]

    Aleks Kissinger and Vladimir Zamdzhiev. 2015. Quantomatic: A Proof Assistant for Diagrammatic Reasoning. In Automated Deduction - CADE-25 , Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham, 326–336

    2015

  30. [39]

    Dexter Kozen. 1997. Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19, 3 (May 1997), 427–443. https: //doi.org/10.1145/256167.256195

    1997

  31. [40]

    Adrian Lehmann, Ben Caldwell, and Robert Rand. 2022. VyZX : A Vision for Verifying the ZX Calculus. arXiv:2205.05781 [quant-ph] https://arxiv.org/abs/2205.05781

    2022 arXiv

  32. [41]

    Adrian Lehmann, Ben Caldwell, Bhakti Shah, and Robert Rand. 2023. VyZX: Formal Verification of a Graphical Quantum Language. arXiv:2311.11571 [cs.PL] https://arxiv.org/abs/2311.11571

    2023 arXiv

  33. [42]

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

    2023 doi

  34. [43]

    Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. 2019. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International P...

    2019

  35. [44]

    Assia Mahboubi and Enrico Tassi. 2022. Mathematical Components. Zenodo. https://doi.org/10.5281/zenodo.7118596

    2022 doi

  36. [45]

    Hynek Mlnarık. 2007. Quantum programming language LanQ. Masaryk University-Faculty of Informatics, Czech Republic (2007)

    2007

  37. [46]

    Carroll Morgan. 1990. Programming from specifications. Prentice-Hall, Inc., USA

    1990

  38. [47]

    Oliveira

    Ana Neri, Rui Soares Barbosa, and José N. Oliveira. 2022. Compiling Quantamorphisms for the IBM Q Experience. IEEE Transactions on Software Engineering 48, 11 (2022), 4339–4356. https://doi.org/10.1109/TSE.2021.3117515 ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article ....

    2022

  39. [48]

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

    2010

  40. [49]

    Bernhard Ömer. 2005. Classical Concepts in Quantum Programming. International Journal of Theoretical Physics 44, 7 (01 Jul 2005), 943–955. https://doi.org/10.1007/s10773-005-7071-x

    2005 doi

  41. [50]

    Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: a core language for quantum circuits. InProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (...

    2017

  42. [51]

    Anurudh Peduri, Ina Schaefer, and Michael Walter. 2025. QbC: Quantum Correctness by Construction. Proc. ACM Program. Lang. 9, OOPSLA1, Article 99 (April 2025), 29 pages. https://doi.org/10.1145/3720433

    2025 doi

  43. [52]

    Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, and Xiaodi Wu

  44. [53]

    Yuxiang Peng, Mingsheng Ying, and Xiaodi Wu. 2022. Algebraic reasoning of Quantum programs via non-idempotent Kleene algebra (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 657–670. https://doi.org/10. 1145/3519939.3523713

    2022

  45. [54]

    Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic. 2018. ReQWIRE: Reasoning about Reversible Quantum Circuits. In Proceedings 15th International Conference on Quantum Physics and Logic, QPL 2018, Halifax, Canada, 3-7th June 2018 (EPTCS, Vol. 287) , Peter Selinger ...

    2018

  46. [55]

    Robert Rand, Jennifer Paykin, and Steve Zdancewic. 2017. QWIRE Practice: Formal Verification of Quantum Circuits in Coq. In Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017, Nijmegen, The Netherlands, 3-7 July 2017. (EPTCS, Vol. 266) , Bob Coeck...

    2017 doi

  47. [56]

    Roscoe and C.A.R

    A.W. Roscoe and C.A.R. Hoare. 1988. The laws of OCCAM programming. Theoretical Computer Science 60, 2 (1988), 177–229. https://doi.org/10.1016/0304-3975(88)90049-7

    1988 doi

  48. [57]

    Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzotto. 2018. From Symmetric Pattern-Matching to Quantum Control. In Foundations of Software Science and Computation Structures , Christel Baier and Ugo Dal Lago (Eds.). Springer International Publishing, Cham, 348–364

    2018

  49. [58]

    J. W. Sanders and P. Zuliani. 2000. Quantum Programming. InMathematics of Program Construction, Roland Backhouse and José Nuno Oliveira (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 80–99

    2000

  50. [59]

    Bhakti Shah, William Spencer, Laura Zielinski, Ben Caldwell, Adrian Lehmann, and Robert Rand. 2024. ViCAR: Visualizing Categories with Automated Rewriting in Coq. arXiv:2404.08163 [cs.PL] https://arxiv.org/abs/2404.08163

    2024

  51. [60]

    Shende, Stephen S

    Vivek V. Shende, Stephen S. Bullock, and Igor L. Markov. 2005. Synthesis of quantum logic circuits. In Proceedings of the 2005 Asia and South Pacific Design Automation Conference (Shanghai, China) (ASP-DAC ’05). Association for Computing Machinery, New York, NY, USA, 272–275. ...

    2005

  52. [61]

    Seyon Sivarajah, Silas Dilkes, Alexander Cowtan, Will Simmons, Alec Edgington, and Ross Duncan. 2020. t|ket〉: a retargetable compiler for NISQ devices. Quantum Science and Technology 6, 1 (nov 2020), 014003. https://doi.org/10. 1088/2058-9565/ab8e92

    2020

  53. [62]

    Sam Staton. 2015. Algebraic Effects, Linearity, and Quantum Programming Languages. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Mumbai, India) (POPL ’15). Association for Computing Machinery, New York, NY, USA, 395–406. ...

    2015

  54. [63]

    Korbinian Staudacher. 2021. Optimization Approaches for Quantum Circuits using ZX-calculus . Ph. D. Dissertation. Master’s thesis, Ludwig-Maximilians-Universität, München. Available at https

    2021

  55. [64]

    Steiger, Thomas Häner, and Matthias Troyer

    Damian S. Steiger, Thomas Häner, and Matthias Troyer. 2018. ProjectQ: an open source software framework for quantum computing. Quantum 2 (Jan. 2018), 49. https://doi.org/10.22331/q-2018-01-31-49

    2018 doi

  56. [65]

    Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler. 2018. Q#: Enabling Scalable Quantum Computing and Develop- ment with a High-level DSL. In Proceedings of the Rea...

    2018

  57. [67]

    The Coq Development Team. 2023. The Coq Proof Assistant . https://doi.org/10.5281/zenodo.8161141

    2023 doi

  58. [68]

    The MathComp Analysis Development Team. 2024. MathComp-Analysis: Mathematical Components compliant Analysis Library. https://github.com/math-comp/analysis. Since 2017. Version 1.0.0. ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article . Publication date: September 2025. 3...

    2024

  59. [69]

    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

  60. [70]

    Dominique Unruh. 2020. Post-Quantum Verification of Fujisaki-Okamoto. In Advances in Cryptology – ASIACRYPT 2020, Shiho Moriai and Huaxiong Wang (Eds.). Springer International Publishing, Cham, 321–352

    2020

  61. [71]

    Benoît Valiron. 2022. Semantics of quantum programming languages: Classical control, quantum control. Journal of Logical and Algebraic Methods in Programming 128 (2022), 100790. https://doi.org/10.1016/j.jlamp.2022.100790

    2022

  62. [72]

    Viamontes, Igor L

    George F. Viamontes, Igor L. Markov, and John P. Hayes. 2007. Checking equivalence of quantum circuits and states. In 2007 IEEE/ACM International Conference on Computer-Aided Design. 69–74. https://doi.org/10.1109/ICCAD.2007.4397246

    2007

  63. [73]

    Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks. 2023. Qunity: A Unified Language for Quantum and Classical Computing. Proc. ACM Program. Lang. 7, POPL, Article 32 (jan 2023), 31 pages. https://doi.org/10.1145/3571225

    2023 doi

  64. [74]

    Amanda Xu, Abtin Molavi, Lauren Pick, Swamit Tannu, and Aws Albarghouthi. 2023. Synthesizing Quantum-Circuit Optimizers. Proc. ACM Program. Lang. 7, PLDI, Article 140 (jun 2023), 25 pages. https://doi.org/10.1145/3591254

    2023 doi

  65. [75]

    Acar, and Zhihao Jia

    Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, and Zhihao Jia. 2022. Quartz: superoptimization of Quantum circuits (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 625–640. ht...

    2022

  66. [76]

    Zhaowei Xu, Mingsheng Ying, and Benoît Valiron. 2021. Reasoning about recursive quantum programs. arXiv:2107.11679 [cs.PL]

    2021 arXiv

  67. [77]

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

    2016

  68. [78]

    Mingsheng Ying, Nengkun Yu, and Yuan Feng. 2012. Defining Quantum Control Flow. arXiv:1209.4379 [quant-ph]

    2012 arXiv

  69. [79]

    Mingsheng Ying and Zhicheng Zhang. 2023. Quantum Recursive Programming with Quantum Case Statements. arXiv:2311.01725 [cs.PL] https://arxiv.org/abs/2311.01725

    2023 arXiv

  70. [80]

    Mingsheng Ying and Zhicheng Zhang. 2024. Verification of Recursively Defined Quantum Circuits. arXiv:2404.05934 [quant-ph] https://arxiv.org/abs/2404.05934

    2024 arXiv

  71. [81]

    Nengkun Yu. 2023. Structured theorem for quantum programs and its applications. ACM Transactions on Software Engineering and Methodology 32, 4, Article 103 (2023), 35 pages

    2023

  72. [82]

    Charles Yuan and Michael Carbin. 2024. The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation. Proc. ACM Program. Lang. 8, PLDI, Article 167 (June 2024), 26 pages. https://doi.org/10.1145/3656397

    2024 doi

  73. [83]

    Charles Yuan, Agnes Villanyi, and Michael Carbin. 2024. Quantum Control Machine: The Limits of Control Flow in Quantum Programming. Proc. ACM Program. Lang. 8, OOPSLA1, Article 94 (apr 2024), 28 pages. https://doi.org/10. 1145/3649811

    2024

  74. [84]

    Zhicheng Zhang and Mingsheng Ying. 2025. Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs. Proc. ACM Program. Lang. 8, PLDI (June 2025). https://doi.org/10.1145/3729283

    2025 doi

  75. [85]

    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, Article 29 (jan 2023), 33 pages. https://doi.org/10.1145/3571222

    2023 doi

  76. [86]

    Paolo Zuliani. 2005. Compiling quantum programs. Acta Informatica 41, 7 (01 Jun 2005), 435–474. https://doi.org/10. 1007/s00236-005-0165-3

    2005

  77. [87]

    ⇒”: This is immediate, since𝐴⊥𝐵 means𝐴𝐵 = 0. “⇐

    Paolo Zuliani et al. 2004. Non-deterministic quantum programming. In Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL) , Vol. 33. TUCS, 179–195. ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article . Publication date: September 2025. Laws...

    2004

  78. [89]

    =𝑀0𝑁1𝜌𝑁† 1𝑀† 0 = 0, E1(𝑁1𝜌𝑁†

  79. [90]

    =𝑀1𝑁1𝜌𝑁† 1𝑀† 1 =𝑁1𝜌𝑁† 1, from the assumption of𝑀∝𝑁 and Lemma A.2. Together with Proposition 3.1(4–6), this yields: ⟦𝑁▷(𝑃;(𝑀∗𝑃))⟧(𝜌) =𝑁0𝜌𝑁† 0+⟦𝑃;(𝑀∗𝑃)⟧ 𝑁1𝜌𝑁† 1 =𝑁0𝜌𝑁† 0+ ∞∑︁ 𝑛=0 (E0◦(⟦𝑃⟧◦E 1)𝑛) ⟦𝑃⟧(𝑁1𝜌𝑁† 1) =𝑁0𝜌𝑁† 0+ ∞∑︁ 𝑛=0 (E0◦(⟦𝑃⟧◦E 1)𝑛) ⟦𝑃⟧(E 1(𝑁1𝜌𝑁† 1)) =𝑁0𝜌𝑁† 0+ ∞∑︁ 𝑛=0 E...

    2025

  80. [91]

    =𝑀0𝑁1𝜌𝑁† 1𝑀† 0 =(𝑀⊥)0𝑁1𝜌𝑁† 1(𝑀⊥)† 1 =𝑁1𝜌𝑁† 1, E1(𝑁1𝜌𝑁†

  81. [92]

    =𝑀1𝑁1𝜌𝑁† 1𝑀† 1 =(𝑀⊥)0𝑁1𝜌𝑁† 1(𝑀⊥)† 0 = 0, from the assumption of𝑀⊥∝𝑁 and Lemma A.2. Therefore, by Proposition 3.1(5, 6) we have: ⟦𝑁▷(𝑀∗𝑃)⟧(𝜌) =𝑁0𝜌𝑁† 0+⟦𝑀∗𝑃⟧ 𝑁1𝜌𝑁† 1 =𝑁0𝜌𝑁† 0+ ∞∑︁ 𝑛=0 (E0◦(⟦𝑃⟧◦E 1)𝑛) 𝑁1𝜌𝑁† 1 =𝑁0𝜌𝑁† 0+E 0 𝑁1𝜌𝑁† 1 + ∞∑︁ 𝑛=1 E0◦(⟦𝑃⟧◦E 1)𝑛−1 ⟦𝑃⟧ E1 𝑁1𝜌𝑁† 1 =𝑁0𝜌𝑁† 0+...

    2025

  82. [2023]

    Proceedings of the National Academy of Sciences 120, 21 (2023), e2218775120

    A formally certified end-to-end implementation of Shor’s factorization algorithm. Proceedings of the National Academy of Sciences 120, 21 (2023), e2218775120. https://doi.org/10.1073/pnas.2218775120 arXiv:https://www.pnas.org/doi/pdf/10.1073/pnas.2218775120

    2023 doi

Pith tools

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