Pith. sign in

REVIEW 2 major objections 5 minor 37 references

D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation

T0 review · 2 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read D-Hammer proves labelled Dirac equalities by sound normalization and a label-elimination theorem.

desk verdict D-Hammer is a real step forward for automated reasoning in labelled Dirac notation, but the normalization's confluence claim in Appendix E is unproven and my quick example suggests CheckEq can return false negatives. read the letter →

arxiv 2505.08633 v1 pith:ISD2345W submitted 2025-05-13 cs.PL

Yingte Xu , Li Zhou , Gilles Barthe This is my paper · ORCID
classification cs.PL MSC 68Q4203B3568N3081P68
keywords labelledDiracnotationbra-ketequationalreasoningtermnormalizationquantumprogramverificationdependentlytypedlanguagesoundnessSUM-SWAP
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 presents D-Hammer, a tool that automates equational reasoning in labelled Dirac notation, the bra-ket formalism used for many-body quantum states and quantum program assertions. It defines a dependently typed, higher-order language for such expressions, gives it a Hilbert-space denotational semantics, and proves that the equational proof system is sound with respect to that semantics. The central technical result is a label-elimination theorem showing that equality between labelled expressions reduces, soundly and completely, to equality between plain Dirac expressions. The tool then checks plain equality with a normalizing rewrite engine that handles associative-commutative symbols, summation swapping, and alpha-equivalence. The paper evaluates the implementation on textbook examples, a large Coq formalization benchmark, and labelled examples including a hard quantum separation logic identity.

What carries the argument

The engine is a normalization algorithm that reduces equivalence modulo the axiom sets R and E to syntactic identity. It uses term rewriting for the R rules, including definition expansion, scalar and linear algebra, delta elimination, and sum pushing, then handles the E axioms with three specialized passes: sorting terms by an order that treats all bound variables as equal, reordering successive summations by the first appearance of their bound variables, and converting to de Bruijn indices to eliminate alpha-equivalence. The key design point is that sorting is done before summation order is fixed, because bound-variable names can be permuted freely in a successive sum. For labelled expressions, register-indexed kets, bras, and operators are expanded into big sums of labelled basis tensors, and sorting rules eliminate matching bra-ket pairs, eventually producing a plain Dirac expression.

What would settle it

Find two well-typed, semantically equal labelled expressions, such as the same summation body written under different nested orders of the same bound variables, and check whether D-Hammer normalizes them to different normal forms; a counterexample would refute the normalizer's completeness and make 'not equal' answers unreliable.

Watch

Extended reading notes

Core claim

The paper's central claim is that equational proofs in labelled Dirac notation can be automated without losing semantic fidelity. D-Hammer's language separates indices, types, and terms, and interprets expressions in Hilbert spaces with the tensor product as an associative-commutative symbol. Theorem 1 states soundness: any equation provable from the axioms is valid in the denotational semantics. Theorem 2 states that for labelled expressions without free variables of the labelled type, eliminating labels—expanding registers to basis sums, rewriting to a normal form, then ordering and stripping labels—preserves semantic equality in both directions: Γ⊨D₁=D₂ iff Γ⊨e₁=e₂ for the translated plain equations. So the proof burden for labelled notation is reduced to proving plain Dirac equalities, and those are handled by a normalization algorithm that fully rewrites modulo the axiom set.

Load-bearing premise

The load-bearing premise is that the normalization algorithm is a full normalizer: any two expressions equivalent under the axioms reduce to the same syntactic normal form, and the paper asserts this for the AC and summation-swap passes without giving a confluence proof.

Editorial extensions

If this is right

  • Every equation D-Hammer reports as equal is genuinely valid in the Hilbert-space semantics, by Theorem 1.
  • Labelled equalities can be checked by eliminating labels and running the plain normalizer, by the iff reduction of Theorem 2.
  • On the plain Dirac benchmark, D-Hammer verifies 158 ported examples from a Coq formalization in under ten seconds, whereas the prior tool takes more than 45 seconds for 156 examples.
  • The labelled examples include LDN-10, a seven-register quantum separation logic identity that is difficult to write or prove without labels, solved in about five seconds.
  • The tool is not competitive with specialized quantum circuit equivalence checkers, and the authors state that D-Hammer makes no completeness claim for its rewriting theory.

Reading between the lines

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

  • If the normalization algorithm were proved confluent and terminating, D-Hammer would become a decision procedure for its equational theory; the paper currently proves soundness and semantic label elimination but not completeness of the normalizer.
  • The two-phase sort-then-swap strategy for handling AC symbols and permutable summations may transfer to other formalisms where associative-commutative operators coexist with reorderable binders.
  • D-Hammer's rewriting traces are a natural starting point for machine-checkable certificates, which would let a proof assistant independently confirm each reported equality.
  • The label-elimination reduction suggests that labelled formalisms can often be implemented as a thin layer over an efficient plain normalizer, rather than requiring a purpose-built labelled rewriting engine.
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

2 major / 5 minor

Summary. The paper presents D-Hammer, a C++ implementation of an equational prover for plain and labelled Dirac notation. The formal language is a higher-order, dependently typed calculus with AC symbols of indefinite arity, and expressions are interpreted as linear maps between Hilbert spaces over finite index sets. The paper states a soundness theorem (Theorem 1) for the equational axioms and a label-elimination theorem (Theorem 2) that reduces equality of labelled expressions to equality of plain expressions. Normalization consists of rewriting rules and three specialized steps: sorting modulo AC while ignoring bound variables, reordering nested summations, and de Bruijn conversion. The implementation is evaluated on 18 textbook examples, 158 CoqQ examples, six labelled-Dirac examples, and six small quantum-circuit equivalences, with a claimed speedup over DiracDec on the CoqQ subset.

Significance. If the completeness claims were established, this would be a useful contribution: labelled Dirac notation is central to several quantum Hoare logics, and automated equality checking would relieve a real bottleneck. The paper's strengths include a typed formalization with a denotational semantics, a proof sketch of Theorem 1, a detailed soundness argument for the label-elimination rules in Appendix D.1, external benchmarks with no fitted parameters, and an open-source implementation. The weakness is that the normalizer's confluence and uniqueness, which would make CheckEq complete, are asserted rather than proven, and the tie-breaking issue in Section E can produce false negatives.

major comments (2)
  1. [Section 3.4 / Appendix E (Definitions 12–14)] The claimed uniqueness of the normal form modulo AC plus SUM-SWAP is unsupported and, as stated, false. Definition 12 treats all bound variables as equal under =B, and Algorithm 1 in Definition 13 sorts arguments by <B without specifying how ties between =B-equal arguments are broken; a stable sort preserves their original order. Let X = sum_{i in s1} sum_{j in s2} ((<i|A|j> * <j|B|i>) + (<j|A|i> * <i|B|j>)) and Y = sum_{j in s2} sum_{i in s1} ((<j|A|i> * <i|B|j>) + (<i|A|j> * <j|B|i>)). These are semantically equal by one application of SUM-SWAP and commutativity of +. After Step 4, both sum bodies contain two =B-equal summands; a stable sort leaves X with the i-first summand first and Y with the j-first summand first. Step 5 then orders the two summations by first occurrence of bound variables, producing different nestings (sum_{s1} sum_{s2} versus sum_{s2} sum_{s1}), and after de Bruijn conversion the additive terms remain in opposite order. The two normal forms are syntactically different, so CheckEq can report 'not equal' for a valid equation. This directly undermines the paper's assertion in Section 3.4 that the normalization is full rather than partial.
  2. [Section 3.4 and Section E] The correctness of the normalization algorithm is load-bearing but is never proved. The text asserts that Steps 4–6 'fully normalize' terms on R union E and that the transformations yield a unique normal form, but Section E contains only definitions and worked examples: there is no termination proof for the sort/swap transformations, no confluence proof for their interaction, and no argument that the final de Bruijn form is independent of the order in which Steps 4 and 5 are applied. Because CheckEq decides equality by comparing normal forms, this missing proof is exactly what would justify the tool's completeness. The soundness of 'equal' answers is not affected, since same normal form plus sound rewrites implies semantic equality, but the capability claim of providing automated equational proof requires completeness. The authors should either supply a rigorous proof for the exact algorithm, including a deterministic tie-breaking rule, or explicitly present D-Hammer as a sound but possibly incomplete normalizer.
minor comments (5)
  1. [Section 3.4, Step 4] Typo: 'cannot alwasy' should be 'cannot always'.
  2. [Table in Section 6] The column header 'expressable' should be 'expressible', and the CoqQ paragraph should explicitly state that the comparison is on the 158 examples expressible in D-Hammer; the remaining four DiracDec-expressible examples are not ported, so the headline speedup is on a restricted set.
  3. [Appendix D.1] The proof repeatedly refers to 'the form of Eqn. (1)' when the displayed normal form it establishes is Eqn. (2) of Section 4.2; the cross-reference should be corrected.
  4. [Appendix D.1, footnote 5] The footnote pointing out a naming typo in Table 21 should be resolved by renaming the rule in the table, not by annotating the proof.
  5. [Definition 13] The pseudocode line 'ls := ls sorted by <B' should specify the sorting algorithm's tie-breaking behavior (e.g., stable sort or a total order on de Bruijn forms); the implementation's behavior is currently under-specified.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the main theorems are proved directly from the denotational semantics and rewriting rules, and the evaluation compares against external benchmarks.

full rationale

D-Hammer's central claims are Theorem 1 (soundness of the equational theory) and Theorem 2 (label elimination). Theorem 1 is proved by checking each axiom and rule against the denotational semantics defined in Appendix B; no benchmark equation or tool output is fed back into the axiom set. Theorem 2 is proved in Appendix D.1 by induction on labelled Dirac expressions, with each rewriting rule's soundness established semantically and no appeal to a prior uniqueness theorem. The normalization procedure in Section E contains an unproved confluence/uniqueness assertion (the iff characterization of =B and the claimed unique normal form), which is a completeness/correctness risk if false, but it is not circular: the 'equal' answers remain sound via Theorem 1 even if normalization is incomplete. The comparison with DiracDec [34] is the authors' own prior tool, but it is used as an empirical baseline on independent, externally sourced examples (QCQI, CoqQ, and literature cases), and the speed-up is measured, not derived from definitions. No fitted parameter is renamed as a prediction, and no ansatz is imported via self-citation. The self-citations that exist (DiracDec, CoqQ) supply background and benchmarks, not the load-bearing justification for the paper's theorems.

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

The central claim relies on standard finite-dimensional Hilbert space semantics, finite index sets, a default ordering of registers, and the absence of labelled-type variables in the target equations. No free parameters are fitted and no new physical entities are introduced.

assumptions (4)
  • domain assumption All base index sets are finite; U(σ) is the finite universal set for σ.
    The semantics in Appendix B interprets indices as finite sets and sums range over U(σ). This matches finite-dimensional quantum systems used in quantum programming but excludes infinite-dimensional Hilbert spaces.
  • standard math Hilbert space semantics with standard linear algebra, tensor/Kronecker products, inner products, and adjoints.
    The denotational semantics in Section 3.3 and Appendix B takes these as given; soundness of axioms relies on linearity and AC properties.
  • domain assumption A default order on quantum variables, such as alphabetical order, exists and is used to define SWAP operators.
    Definition 8 in Section 4.1 equips registers with a default order; the semantics of labelled tensors and lifting depend on this order.
  • domain assumption Expressions being checked contain no free variables of type D(·,·), the labelled Dirac type.
    Theorem 2 (Label Elimination) states its result only for expressions with no variables of type D(·,·); the reduction to plain Dirac notation relies on this restriction.

how reviews work

0 comments
Cite this review

Pith. "Pith review of D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation." pith.science (2026). https://pith.science/paper/ISD2345W

@misc{pith2026250508633,
  author       = {Pith},
  title        = {Pith review of: D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ISD2345W}},
  note         = {Machine review of arXiv:2505.08633}
}
read the original abstract

Labelled Dirac notation is a formalism commonly used by physicists to represent many-body quantum systems and by computer scientists to assert properties of quantum programs. It is supported by a rich equational theory for proving equality between expressions in the language. These proofs are typically carried on pen-and-paper, and can be exceedingly long and error-prone. We introduce D-Hammer, the first tool to support automated equational proof for labelled Dirac notation. The salient features of D-Hammer include: an expressive, higher-order, dependently-typed language for labelled Dirac notation; an efficient normalization algorithm; and an optimized C++ implementation. We evaluate the implementation on representative examples from both plain and labelled Dirac notation. In the case of plain Dirac notation, we show that our implementation significantly outperforms DiracDec.

Figures

Figures reproduced from arXiv: 2505.08633 by the authors.

Figure 1
Figure 1. A normalization outline for the left-hand side of Equation (1). Matched sub￾terms are marked with colors. Blue marking represents variable expansion, red marking represents rule applications, and brown marking represents normalization step 4-6. 4 Labelled Dirac Notation In this section, we extend the language by allowing quantum variables to indicate the quantum system on which vectors and operators act. As discusse… view at source ↗
Figure 2
Figure 2. Time comparison between DiracDec and D-Hammer on the CoqQ benchmark [PITH_FULL_IMAGE:figures/full_fig_p016_2.png] view at source ↗
Figure 3
Figure 3. Part of examples for labelled Dirac notations. See Section F for the full list [PITH_FULL_IMAGE:figures/full_fig_p017_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Time consumptions (in seconds) for quantum circuit equivalence checking using different tools. (circuit) Rx( π 2 ) Rx( π 2 ) T = H Z H T H H (notation) (Rx(π/2) ⊗ 1O) · (1O ⊗ T) · (Rx(π/2) ⊗ 1O) =(1O ⊗ H) · (1O ⊗ H) · (H ⊗ 1O) · (Z ⊗ 1O) · (H ⊗ 1O) · (1O ⊗ T) [PITH_FU…
Figure 5
Figure 5. Figure 5: The quantum circuit and Dirac notation encoding for example QC-5. 7 Related Work Comparison with DiracDec Xu et al [34] define a language and an associate and commutative rewriting system for Dirac notation, and implement their language and rewriting system in Mathemat…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

37 extracted references · 11 canonical work pages

  1. [1]

    Abdulla, P.A., Chen, Y.G., Chen, Y.F., Holík, L., Lengál, O., Lin, J.A., Lo, F.Y., Tsai, W.L.: Verifying quantum circuits with level-synchronized tree au- tomata. Proc. ACM Program. Lang.9(POPL) (Jan 2025). https://doi.org/10. 1145/3704868, https://doi.org/10.1145/3704868

    doi:10.1145/3704868 2025

  2. [2]

    In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings

    Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings. pp. 415–425. IEEE Computer Society (2004). https://doi.org/10.1109/LICS.2004.1319636, https://doi.org/10.1109/LICS.2004. 1319636

    arXiv 2004

  3. [3]

    In: 2023 IEEE 64th Annual Symposium on Foundations of Computer Science (FOCS)

    Acuaviva, A., Makam, V., Nieuwboer, H., Pérez-García, D., Sittner, F., Walter, M., Witteveen, F.: The minimal canonical form of a tensor network. In: 2023 IEEE 64th Annual Symposium on Foundations of Computer Science (FOCS). p. 328–362. IEEE (Nov 2023). https://doi.org/10.1109/focs57990.2023.00027, http: //dx.doi.org/10.1109/FOCS57990.2023.00027

    arXiv 2023

  4. [4]

    Electronic Proceedings in Theoretical Computer Science287, 1–21 (Jan 2019)

    Amy, M.: Towards large-scale functional verification of universal quantum circuits. Electronic Proceedings in Theoretical Computer Science287, 1–21 (Jan 2019). https://doi.org/10.4204/eptcs.287.1, http://dx.doi.org/10.4204/EPTCS.287.1

    doi:10.4204/eptcs.287.1 2019

  5. [5]

    New Journal of Physics16(9), 093021 (2014)

    Backens, M.: The zx-calculus is complete for stabilizer quantum mechanics. New Journal of Physics16(9), 093021 (2014)

    work page 2014

  6. [6]

    Barbosa, H., Barrett, C.W., Cook, B., Dutertre, B., Kremer, G., Lachnitt, H., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Tinelli, C., Zohar, Y.: Generating and exploiting automated reasoning proof certificates. Commun. ACM66(10), 86–95 (2023). https://doi.org/10.1145/3587692, https://doi.org/10. 1145/3587692

    doi:10.1145/3587692 2023

  7. [7]

    In: Proceedings of the 26th Asia and South Pacific Design Automation Conference

    Burgholzer,L.,Kueng,R.,Wille,R.:Randomstimuligenerationfortheverification of quantum circuits. In: Proceedings of the 26th Asia and South Pacific Design Automation Conference. p. 767–772. ASPDAC ’21, Association for Computing Machinery,NewYork,NY,USA(2021).https://doi.org/10.1145/3394885.3431590, https://doi.org/10.1145/3394885.3431590

    arXiv 2021

  8. [8]

    In: Akleylek, S., Dundua, B

    Chareton, C., Lee, D., Valiron, B., Vilmart, R., Bardin, S., Xu, Z.: Formal methods for quantum algorithms. In: Akleylek, S., Dundua, B. (eds.) Handbook of Formal Analysis and Verification in Cryptography, pp. 319–422. CRC Press (2023). https: //doi.org/10.1201/9781003090052-7, https://doi.org/10.1201/9781003090052-7

    doi:10.1201/9781003090052-7 2023

Show all 37 references
  1. [9]

    In: Enea, C., Lal, A

    Chen, Y.F., Chung, K.M., Lengál, O., Lin, J.A., Tsai, W.L.: Autoq: An automata- based quantum circuit verifier. In: Enea, C., Lal, A. (eds.) Computer Aided Veri- fication. pp. 139–153. Springer Nature Switzerland, Cham (2023)

    2023

  2. [10]

    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 cir- cuits. Proc. ACM Program. Lang.7(PLDI) (Jun 2023). https://doi.org/10.1145/ 3591270, https://doi.org/10.1145/3591270

    2023 doi

  3. [11]

    Cirac, J.I., Pérez-García, D., Schuch, N., Verstraete, F.: Matrix product states and projected entangled pair states: Concepts, symmetries, theorems. Rev. Mod. Phys. 93, 045003 (Dec 2021). https://doi.org/10.1103/RevModPhys.93.045003, https:// link.aps.org/doi/10.1103/RevModPh...

    2021 doi

  4. [12]

    In: Szeider, S., Ganian, R., Silva, A

    Clément, A., Heurtel, N., Mansfield, S., Perdrix, S., Valiron, B.: LOv-Calculus: A Graphical Language for Linear Optical Quantum Circuits. In: Szeider, S., Ganian, R., Silva, A. (eds.) 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Le...

    2022

  5. [13]

    In: 38th Annual ACM/IEEE Sympo- sium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29,

    Clément, A., Heurtel, N., Mansfield, S., Perdrix, S., Valiron, B.: A complete equational theory for quantum circuits. In: 38th Annual ACM/IEEE Sympo- sium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29,

    2023

  6. [14]

    In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I

    Coecke, B., Duncan, R.: Interacting quantum observables. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008...

    2008

  7. [15]

    New Journal of Physics13(4), 043016 (2011)

    Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New Journal of Physics13(4), 043016 (2011)

    2011

  8. [16]

    Indagationes Mathematicae (Proceedings)75(5), 381–392 (1972)

    de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for au- tomatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings)75(5), 381–392 (1972). https://doi.org/ https://doi.org/10.1016/1385-7258(72)90034-...

    1972

  9. [17]

    In: Mathematical pro- ceedings of the Cambridge philosophical society

    Dirac, P.A.M.: A new notation for quantum mechanics. In: Mathematical pro- ceedings of the Cambridge philosophical society. vol. 35, pp. 416–418. Cambridge University Press (1939). https://doi.org/10.1017/S0305004100021162

    1939 doi

  10. [18]

    In: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science

    Hadzihasanovic, A.: A diagrammatic axiomatisation for qubit entanglement. In: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 573–584 (2015). https://doi.org/10.1109/LICS.2015.59

    2015 doi

  11. [21]

    In: Dawar, A., Grädel, E

    Jeandel, E., Perdrix, S., Vilmart, R.: Diagrammatic reasoning beyond clifford+t quantum mechanics. In: Dawar, A., Grädel, E. (eds.) Proceedings of the 33rd An- nual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 569–578. ACM (2018...

    2018

  12. [22]

    In: Coecke, B., Leifer, M

    Kissinger, A., van de Wetering, J.: PyZX: Large Scale Automated Diagram- matic Reasoning. In: Coecke, B., Leifer, M. (eds.) Proceedings 16th International Conference on Quantum Physics and Logic, Chapman University, Orange, CA, USA., 10-14 June 2019. Electronic Proceedings in ...

    2020

  13. [23]

    Le, X.B., Lin, S.W., Sun, J., Sanan, D.: A quantum interpretation of separat- ing 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

    2022 doi

  14. [24]

    CoRRabs/2110.01320(2021), https://arxiv.org/ abs/2110.01320

    Lewis, M., Soudjani, S., Zuliani, P.: Formal verification of quantum programs: Theory, tools and challenges. CoRRabs/2110.01320(2021), https://arxiv.org/ abs/2110.01320

    2021 arXiv

  15. [25]

    Li, L., Zhu, M., Cleaveland, R., Nicolellis, A., Lee, Y., Chang, L., Wu, X.: Qafny: A quantum-program verifier (2024), https://arxiv.org/abs/2211.06411

    2024 arXiv

  16. [26]

    Cambridge university press (2010)

    Nielsen, M.A., Chuang, I.L.: Quantum computation and quantum information. Cambridge university press (2010)

    2010

  17. [27]

    Linear Algebra and its Applications694, 206–261 (2024)

    Palsberg, J., Yu, N.: Optimal implementation of quantum gates with two controls. Linear Algebra and its Applications694, 206–261 (2024). https://doi.org/https://doi.org/10.1016/j.laa.2024.03.039, https://www. sciencedirect.com/science/article/pii/S0024379524001356

    2024 doi

  18. [28]

    IEEE Journal on Emerging and Selected Topics in Cir- cuits and Systems12(3), 662–675 (2022)

    Peham, T., Burgholzer, L., Wille, R.: Equivalence checking of quantum circuits with the zx-calculus. IEEE Journal on Emerging and Selected Topics in Cir- cuits and Systems12(3), 662–675 (2022). https://doi.org/10.1109/JETCAS.2022. 3202204

    2022 doi

  19. [29]

    Perez-Garcia, D., Verstraete, F., Wolf, M.M., Cirac, J.I.: Matrix product state representations (2007), https://arxiv.org/abs/quant-ph/0608197

    2007 arXiv

  20. [30]

    In: 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

    Poór, B., Wang, Q., Shaikh, R.A., Yeh, L., Yeung, R., Coecke, B.: Completeness for arbitrary finite dimensions of zxw-calculus, a unifying calculus. In: 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–14 (2023). https://doi.org/10.1109/LICS56636....

    2023

  21. [31]

    Unruh, D.: Quantum relational hoare logic. Proc. ACM Program. Lang.3(POPL) (Jan 2019). https://doi.org/10.1145/3290346, https://doi.org/10.1145/3290346

    2019 doi

  22. [32]

    van de Wetering, J.: Zx-calculus for the working quantum computer scientist (2020), https://arxiv.org/abs/2012.13966

    2020 arXiv

  23. [33]

    Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: egg: Fast and extensible equality saturation. Proc. ACM Program. Lang.5(POPL), 1–29 (2021). https://doi.org/10.1145/3434304, https://doi.org/10.1145/3434304

    2021 doi

  24. [34]

    ACM Program

    Xu,Y.,Barthe,G.,Zhou,L.:Automatingequationalproofsindiracnotation.Proc. ACM Program. Lang.9(POPL) (Jan 2025). https://doi.org/10.1145/3704878, https://doi.org/10.1145/3704878

    2025 doi

  25. [35]

    Yan, P., Jiang, H., Yu, N.: On incorrectness logic for quantum programs. Proc. ACM Program. Lang.6(OOPSLA1) (Apr 2022). https://doi.org/10.1145/3527316, https://doi.org/10.1145/3527316

    2022 doi

  26. [36]

    Acta Informatica62(1), 7 (Dec 2024)

    Zhong, S.: Birkhoff-von neumann quantum logic enriched with entanglement quan- tifiers: coincidence theorem and semantic consequence. Acta Informatica62(1), 7 (Dec 2024)

    2024

  27. [37]

    In: 36th Annual ACM/IEEE Sympo- sium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2,

    Zhou, L., Barthe, G., Hsu, J., Ying, M., Yu, N.: A quantum interpretation of bunched logic & quantum separation logic. In: 36th Annual ACM/IEEE Sympo- sium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2,

    2021

  28. [38]

    Zhou, L., Barthe, G., Strub, P.Y., Liu, J., Ying, M.: CoqQ: Foundational verifi- cation of quantum programs. Proc. ACM Program. Lang.7(POPL) (jan 2023). https://doi.org/10.1145/3571222, https://doi.org/10.1145/3571222 24 Yingte Xu, Li Zhou, and Gilles Barthe Appendix A Full Ty...

    2023 doi

  29. [2021]

    pp. 1–14. IEEE (2021). https://doi.org/10.1109/LICS52264.2021.9470673, https://doi.org/10.1109/LICS52264.2021.9470673

    2021

Pith tools

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