pith. machine review for the scientific record. sign in

arxiv: 2604.24578 · v1 · submitted 2026-04-27 · 💻 cs.PL

Recognition: unknown

Hybrid Path-Sums for Hybrid Quantum Programs

Christophe Chareton , Jad Issa , Mathieu Nguyen , Nicolas Blanco , S\'ebastien Bardin
Authors on Pith no claims yet

Pith reviewed 2026-05-07 17:17 UTC · model grok-4.3

classification 💻 cs.PL
keywords hybrid quantum programsformal verificationsymbolic executionpath sumsquantum controlclassical controlassertionsrewriting systems
0
0 comments X

The pith

Hybrid Path-Sums give a symbolic representation for verifying hybrid quantum programs that mix quantum and classical control.

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

The paper introduces Hybrid Path-Sums to describe and manipulate sets of states that arise in programs combining quantum gates, measurements, classical instructions, quantum control, and hybrid data structures. It supplies rewriting rules that simplify these representations while preserving their meaning and a small assertion language for stating equivalences between programs, invariants on state components, and probability queries over measurement outcomes. The authors prove that the representation, the rules, and the assertion language are sound and complete for the intended class of programs, then implement the whole system as a symbolic execution engine. This supplies a static-analysis route to checking quantum software whose behavior is otherwise difficult to test by execution.

Core claim

Hybrid Path-Sums constitute a symbolic representation that encodes finite sets of hybrid quantum-classical states, equipped with a rewriting system that reduces expressions while preserving the set of concrete states they denote and with an assertion language that can express program equivalence, state properties, and probabilistic statements; the paper establishes the semantic correctness of the representation, the rewriting rules, and the assertion system.

What carries the argument

Hybrid Path-Sums, a symbolic structure that represents sets of hybrid quantum-classical states and supports rewriting for simplification and semantic reasoning.

If this is right

  • Two hybrid programs can be proved equivalent by reducing both to the same Hybrid Path-Sum.
  • Assertions can extract the probability of any measurement outcome or the satisfaction of any state predicate without enumerating all paths.
  • The rewriting system yields a decision procedure for a useful fragment of hybrid quantum properties.
  • The implemented engine scales to representative case studies drawn from the quantum-computing literature.

Where Pith is reading between the lines

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

  • The same representation could serve as an intermediate language for compiling hybrid programs to different quantum hardware backends.
  • Integration with classical symbolic executors might allow verification of larger classical control logic surrounding quantum kernels.
  • Extending the assertion language to temporal properties would enable checking of sequential hybrid protocols.

Load-bearing premise

The Hybrid Path-Sums representation together with its rewriting rules can capture every reachable hybrid state and every observable behavior that arises in programs containing generic quantum control and arbitrary classical-quantum data.

What would settle it

A concrete hybrid quantum program whose final state distribution or intermediate hybrid state set cannot be exactly reproduced by any sequence of Hybrid Path-Sum rewrites would show the representation is incomplete.

Figures

Figures reproduced from arXiv: 2604.24578 by Christophe Chareton, Jad Issa, Mathieu Nguyen, Nicolas Blanco, S\'ebastien Bardin.

Figure 1
Figure 1. Figure 1: Quantum teleportation circuit Consider the standard quantum teleportation pro￾tocol [9, 66] which moves the state |𝑥⟩𝜓 of a qubit 𝜓 into a qubit 𝑏. Teleportation is an essential building block in quantum information transmis￾sion [13], Measurement-based Quantum Compu￾tation (MBQC) [74], and more. The hybrid circuit for teleportation is given in view at source ↗
Figure 2
Figure 2. Figure 2: Quantum Phase Estimation, code, specification derivation and circuit view at source ↗
Figure 3
Figure 3. Figure 3: Circuit and HPS derivation for the 3-qubit error correction code Note that Step 5 performs successive control on the same measurement results. Therefore, storing that classical data in actual memory cells is unavoidable for this case, a requirement that is missed by most pre-existing solutions (see view at source ↗
Figure 4
Figure 4. Figure 4: Identifiers typing rules Γ ⊢ 𝑟 : Reg Γ ⊢ 𝑖 : Int r[i :] Γ ⊢ 𝑟[𝑖 :] : Reg Γ ⊢ 𝑟 : Reg Γ ⊢ 𝑖 : Int r[: i] Γ ⊢ 𝑟[: 𝑖] : Reg Γ ⊢ 𝑟 : Reg Γ ⊢ 𝑖 : Int Γ ⊢ 𝑗 : Int r[i : j] Γ ⊢ 𝑟[𝑖 : 𝑗] : Reg view at source ↗
Figure 5
Figure 5. Figure 5: Registers typing rules. These rules to be duplicated, once for CReg and once for QReg. view at source ↗
Figure 6
Figure 6. Figure 6: CBool typing rules. Classical booleans are those that are uniform across a given world issued from constants, program parameters, or classical registers. CBool is a subtype of Bool. Technically, three more rules are omitted: ∧, ⊕, and ? which are rules for Bool (figure 7) and under which CBool is closed view at source ↗
Figure 7
Figure 7. Figure 7: Bool typing rules. 𝑏1?𝑏2 : 𝑏3 represents the ternary operator if 𝑏1 then 𝑏2 else 𝑏3. The distinction between CBool and Bool is the appearance of quantum registers. 𝑛 ∈ N N Γ ⊢ 𝑛 : Int 𝑖 ∈ N VarInt Γ ⊢ 𝑥 𝐼 𝑖 : Int Γ ⊢ 𝑖 : Int Γ ⊢ 𝑗 : Int + Γ ⊢ 𝑖 + 𝑗 : Int Γ ⊢ 𝑖 : Int Γ ⊢ 𝑗 : Int ∗ Γ ⊢ 𝑖 ∗ 𝑗 : Int Γ ⊢ 𝑖 : Int Γ ⊢ 𝑗 : Int Exp Γ ⊢ 𝑖 𝑗 : Int view at source ↗
Figure 8
Figure 8. Figure 8: Int typing rules Γ ⊢ 𝑝 : QProg QProg Γ ⊢ 𝑝 : Prog Γ ⊢ 𝑞 : QReg Init Γ ⊢ Init(𝑞) : Prog Γ ⊢ 𝑞 : QReg Γ ⊢ 𝑐 : CReg Measure Γ ⊢ Measure(𝑞, 𝑐) : Prog Γ ⊢ 𝑐1 : CReg Γ ⊢ 𝑐2 : CReg Classical Γ ⊢ 𝑐1 := 𝑓 ( ⌈𝑐2⌉) : Prog Γ ⊢ 𝑝 : Prog Γ ⊢ 𝑞 : Prog seq Γ ⊢ 𝑝;𝑞 : Prog Γ ⊢ 𝑖 : Int Γ ⊢ 𝑗 : Int Γ ⊢ 𝑝 : Prog for Γ ⊢ For 𝑥 𝐼 𝑛 = 𝑖, 𝑗 do {𝑝} : Prog Γ ⊢ 𝑏 : CBool Γ ⊢ 𝑝 : Prog Γ ⊢ 𝑞 : Prog C − if Γ ⊢ If 𝑏 then 𝑝 else 𝑞 end : Prog view at source ↗
Figure 9
Figure 9. Figure 9: Prog typing rules Skip Γ ⊢ Skip : QProg 𝑈 ∈ G Γ ⊢ 𝑞 : QReg Unitary Γ ⊢ Apply 𝑈 (𝑞) : QProg Γ ⊢ qreg(𝑝) ∩ qreg(𝑏) = ∅ Γ ⊢ 𝑏 : Bool Γ ⊢ 𝑝 : QProg Γ ⊢ 𝑞 : QProg Q − if Γ ⊢ If 𝑏 then 𝑝 else 𝑞 end : QProg view at source ↗
Figure 11
Figure 11. Figure 11: Typing rules for the 𝜆−calculus. 𝐿[𝑅] := ∅𝐿[𝑅] | 𝑅 · 𝐿[𝑅] LIST OF R SCHEME creg := ident𝐶 | creg[i :] | creg[: i] | creg[i1 : i2] 𝑄𝑢𝑎𝑛𝑡𝑢𝑚 𝑟𝑒𝑔𝑖𝑠𝑡𝑒𝑟𝑠 qreg := ident𝑄 | qreg[i :] | qreg[: i] | qreg[i1 : i2] 𝐶𝑙𝑎𝑠𝑠𝑖𝑐𝑎𝑙 𝑟𝑒𝑔𝑖𝑠𝑡𝑒𝑟𝑠 b1, b2 := 0 | 1 | 𝑦i | ⌈(c/q)reg[i]⌉ | b1 ∧ b2 | b1 ⊕ b2 Booleans i1, i2 := 𝑛 | ♯ (c/q)reg | i1 +𝑖 i2 | i1 ∗ i2 | i i2 1 Integers su1, su2 := ∅ | {𝑦i} | su1 ∪ su2 | su1 \ su2 HPS suppor… view at source ↗
Figure 12
Figure 12. Figure 12: The grammar for HPS terms view at source ↗
Figure 13
Figure 13. Figure 13: Additional rules of the equational theory stemming from the axioms of the algebraic structure of view at source ↗
read the original abstract

As quantum computing becomes an emerging reality, designing efficient quantum programming capabilities is becoming more and more important. Particularly, the debugging and validation of quantum programs is of paramount importance, as these programs are by definition hard to test. Static analysis and formal verification methods for quantum programs started to emerge a few years now, yet they often miss hybrid quantum/classical reasoning facilities with, e.g., generic quantum control, classical control and classical computation instructions. In this paper, we lay out the foundations of a framework for the automated formal verification of (full) hybrid quantum programs featuring both classical and quantum control, measurement and hybrid data structures. In particular, we propose: (1) a novel symbolic representation for describing and manipulating sets of hybrid quantum/classical states called Hybrid Path-Sums (HPS); (2) a set of rewriting rules providing a rich mechanism for simplifying and reasoning on these symbolic hybrid states, and (3) a core assertion language to specify equivalence of hybrid quantum programs, the satisfaction of properties on (parts of) hybrid states, and the extraction of probabilistic statements about the program behavior. We prove the correctness of the novel symbolic representation, of its rewriting system and of the specification system. Finally, we propose a full implementation of this framework as a dedicated symbolic execution engine for hybrid programs. We present an evaluation of a set of representative hybrid case-studies from the literature, showcasing the advantage of our approach and its efficiency compared to state-of-the-art solutions.

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

0 major / 3 minor

Summary. The paper introduces Hybrid Path-Sums (HPS), a novel symbolic representation for sets of hybrid quantum/classical states. It defines a rewriting system to simplify and reason about these states, a core assertion language for specifying program equivalence, state properties, and probabilistic behaviors, proves the correctness of the HPS representation, the rewriting rules, and the assertion system, and presents a complete implementation as a symbolic execution engine evaluated on representative hybrid quantum program case studies from the literature.

Significance. If the correctness proofs and implementation hold, this work would meaningfully advance formal verification techniques for quantum programs by supporting generic quantum control, classical control, measurements, and hybrid data structures in a unified symbolic framework. The explicit proofs of the representation and rules, together with the dedicated implementation and empirical evaluation, provide a concrete foundation that existing approaches often lack for full hybrid programs.

minor comments (3)
  1. The abstract and introduction would benefit from an explicit list or table of the specific literature case studies used in the evaluation section to allow readers to immediately assess coverage of hybrid control and data features.
  2. Notation for Hybrid Path-Sums (e.g., how classical and quantum components are combined in the sum) should include one or two fully worked small examples immediately after the formal definition to improve readability for readers unfamiliar with path-sum representations.
  3. The evaluation section reports efficiency advantages but does not include a direct comparison of memory usage or state-space size against the state-of-the-art tools mentioned; adding these metrics would strengthen the efficiency claims.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our work on Hybrid Path-Sums, including the recognition of the symbolic representation, rewriting rules, assertion language, correctness proofs, implementation, and evaluation on hybrid quantum program case studies. The recommendation for minor revision is noted, and we will address any editorial or minor issues in the revised version.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper introduces a new symbolic representation called Hybrid Path-Sums together with rewriting rules and an assertion language. Correctness is established via proofs on these definitions using standard formal methods (e.g., structural induction). No step reduces by construction to a fitted input, self-citation chain, or renamed prior result; the central claims are derived directly from the paper's own definitions and are independently validated by the implementation and external case studies.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The framework rests on the definition of a new symbolic state representation whose correctness is asserted via proofs; no free parameters are mentioned.

axioms (1)
  • standard math Standard mathematical axioms for sets, functions, and probability measures
    Invoked to define Hybrid Path-Sums and prove properties of the rewriting system.
invented entities (1)
  • Hybrid Path-Sums (HPS) no independent evidence
    purpose: Symbolic representation for sets of hybrid quantum/classical states
    Newly postulated construct enabling the verification framework.

pith-pipeline@v0.9.0 · 5570 in / 1106 out tokens · 144090 ms · 2026-05-07T17:17:44.584407+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

98 extracted references · 82 canonical work pages · 4 internal anchors

  1. [1]

    Rajeev Acharya, Laleh Aghababaie-Beni, Igor Aleiner, Trond I Andersen, Markus Ansmann, Frank Arute, Kunal Arya, Abraham Asfaw, Nikita Astrakhantsev, Juan Atalaya, et al. 2024. Quantum error correction below the surface code threshold.arXiv preprint arXiv:2408.13687(2024). doi:10.1038/s41586-024-08449-y

    work page doi:10.1038/s41586-024-08449-y 2024

  2. [2]

    Amazon Web Services. 2020. Amazon Braket. https://aws.amazon.com/braket/

    2020

  3. [3]

    Matthew Amy. 2019. Towards Large-scale Functional Verification of Universal Quantum Circuits. InProceedings 15th International Conference on Quantum Physics and Logic, QPL 2018 (Electronic Proceedings in Theoretical Computer Science, Vol. 287), Peter Selinger and Giulio Chiribella (Eds.). EPTCS, Halifax, Canada, 1–21. doi:10.4204/EPTCS.287.1

    work page doi:10.4204/eptcs.287.1 2019

  4. [4]

    Matthew Amy. 2023. Complete equational theories for the sum-over-paths with unbalanced amplitudes. arXiv:2306.16369 [quant-ph] doi:10.4204/EPTCS.384.8

    work page doi:10.4204/eptcs.384.8 2023

  5. [5]

    Arute et al., Quantum supremacy using a programmable superconducting processor, Nature 574, 505 (2019), doi:10.1038/s41586-019-1666-5

    Frank Arute, Kunal Arya, Ryan Babbush, Dave Bacon, Joseph C. Bardin, Rami Barends, Rupak Biswas, Sergio Boixo, Fernando G. S. L. Brandao, David A. Buell, et al. 2019. Quantum supremacy using a programmable superconducting processor.Nature574, 7779 (2019), 505–510. doi:10.1038/s41586-019-1666-5

    work page doi:10.1038/s41586-019-1666-5 2019

  6. [6]

    Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan, Matthijs Muis, Ivan Renison, Keiya Sakabe, Michael Walter, Yingte Xu, and Li Zhou. 2025. A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics.arXiv preprint arXiv:2510.07051(2025). doi:10.48550/arXiv.2510.07051

    work page doi:10.48550/arxiv.2510.07051 2025

  7. [7]

    Fabian Bauer-Marquart, Stefan Leue, and Christian Schilling. 2023. symQV: Automated Symbolic Verification of Quantum Programs. InFormal Methods, Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker (Eds.). Springer International Publishing, Cham, 181–198. doi:10.1007/978-3-031-27481-7_12

    work page doi:10.1007/978-3-031-27481-7_12 2023

  8. [8]

    Patrick Behm, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. 1999. Météor: A Successful Application of B in a Large Project. InProceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM’99), Volume I (Lecture Notes in Computer Science, Vol. 1708), Jeannette M. Wing, Jim Woodcock, and Jim Davies (Eds.). Springer, T...

    work page doi:10.1007/3-540-48119-2_22 1999

  9. [9]

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

    work page doi:10.1103/physrevlett.70.1895 1993

  10. [10]

    Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin T. Vechev. 2020. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. InProceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, Alastair F. Donaldson and Emina Torlak (...

    work page doi:10.1145/3385412.3386007 2020

  11. [11]

    Benjamin Bichsel, Anouk Paradis, Maximilian Baader, and Martin Vechev. 2023. Abstraqt: Analysis of Quantum Circuits via Abstract Stabilizer Simulation.Quantum7 (2023), 1185. doi:10.22331/q-2023-11-20-1185

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

  12. [12]

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

    work page doi:10.1007/s10817-020-09584-7 2021

  13. [13]

    H-J Briegel, Wolfgang Dür, Juan I Cirac, and Peter Zoller. 1998. Quantum repeaters: the role of imperfect local operations in quantum communication.Physical Review Letters81, 26 (1998), 5932. doi:10.1103/PhysRevLett.81.5932

    work page doi:10.1103/physrevlett.81.5932 1998

  14. [14]

    Lukas Burgholzer and Robert Wille. 2021. QCEC: A JKQ tool for quantum circuit equivalence checking.Software Impacts7 (2021), 100051. doi:10.1016/j.simpa.2020.100051

    work page doi:10.1016/j.simpa.2020.100051 2021

  15. [15]

    Lukas Burgholzer and Robert Wille. 2022. Handling non-unitaries in quantum circuit equivalence checking. In Proceedings of the 59th ACM/IEEE Design Automation Conference. 529–534. doi:10.1145/3489517.3530482

    work page doi:10.1145/3489517.3530482 2022

  16. [16]

    Titouan Carette, Yohann D’Anello, and Simon Perdrix. 2021. Quantum Algorithms and Oracles with the Scalable ZX-calculus.arXiv preprint arXiv:2104.01043(2021). doi:10.4204/EPTCS.343.10

    work page doi:10.4204/eptcs.343.10 2021

  17. [17]

    Titouan Carette, Dominic Horsman, and Simon Perdrix. 2019. SZX-Calculus: Scalable Graphical Quantum Reasoning. In44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 138), Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen (Eds.). Schloss Dagstuhl ...

    work page doi:10.4230/lipics.mfcs.2019.55 2019

  18. [18]

    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.Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings12648 (2021), 148–17...

    work page doi:10.1007/978-3-030-72019-3_6 2021

  19. [19]

    Christophe Chareton, Sébastien Bardin, Dong Ho Lee, Benoît Valiron, Renaud Vilmart, and Zhaowei Xu. 2023. Formal methods for quantum programs: a survey.Handbook of Formal Analysis and Verification in Cryptography(2023), 319–422. doi:10.48550/arXiv.2109.06493

    work page doi:10.48550/arxiv.2109.06493 2023

  20. [20]

    Springer Dordrecht, 1988.doi:10.1007/978- 94-009-2871-8

    Kean Chen, Yuhao Liu, Wang Fang, Jennifer Paykin, Xin-Chuan Wu, Albert Schmitz, Steve Zdancewic, and Gushu Li. 2025.Verifying Fault-Tolerance of Quantum Error Correction Codes. Springer Nature Switzerland, 3–27. doi:10.1007/978- 3-031-98685-7_1 Hybrid Path-Sums for Hybrid Quantum Programs 25

    work page doi:10.1007/978- 2025

  21. [21]

    Yu-Fang Chen, Kai-Min Chung, Ondřej Lengál, Jyun-Ao Lin, and Wei-Lun Tsai. 2023. AutoQ: An Automata-Based Quantum Circuit Verifier. InComputer Aided Verification, Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland, Cham, 139–153. doi:10.1007/978-3-031-37709-9_7

    work page doi:10.1007/978-3-031-37709-9_7 2023

  22. [22]

    Yu-Fang Chen, Kai-Min Chung, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, and Di-De Yen. 2023. An automata-based framework for verification and bug hunting in quantum circuits.Proceedings of the ACM on Programming Languages7, PLDI (2023), 1218–1243. doi:10.1145/3591270

    work page doi:10.1145/3591270 2023

  23. [23]

    Feifei Cheng, Sushen Vangeepuram, Henry Allard, Seyed Mohammad Reza Jafari, Alex Potanin, and Liyi Li. 2025. Embedding Quantum Program Verification into Dafny.Proceedings of the ACM on Programming Languages9, OOPSLA2 (2025), 2981–3007. doi:10.1145/3763157

    work page doi:10.1145/3763157 2025

  24. [24]

    Richard Cleve, Artur Ekert, Chiara Macchiavello, and Michele Mosca. 1998. Quantum algorithms revisited.Proceedings of the Royal Society of London. Series A: Mathematical, Physical and Engineering Sciences454, 1969 (1998), 339–354. doi:10.1098/rspa.1998.0164

    work page doi:10.1098/rspa.1998.0164 1998

  25. [25]

    Bob Coecke and Ross Duncan. 2011. Interacting Quantum Observables: Categorical Algebra and Diagrammatics.New Journal of Physics13, 4 (Apr 2011), 043016. doi:10.1088/1367-2630/13/4/043016

    work page doi:10.1088/1367-2630/13/4/043016 2011

  26. [26]

    2017.Picturing quantum processes

    Bob Coecke and Aleks Kissinger. 2017.Picturing quantum processes. Cambridge University Press, Cambridge, United Kingdom

    2017

  27. [27]

    Andrew Cross, Ali Javadi-Abhari, Thomas Alexander, Niel De Beaudrap, Lev S Bishop, Steven Heidel, Colm A Ryan, Prasahnt Sivarajah, John Smolin, Jay M Gambetta, et al. 2022. OpenQASM 3: A broader and deeper quantum assembly language.ACM Transactions on Quantum Computing3, 3 (2022), 1–50. doi:10.1145/3505636

    work page doi:10.1145/3505636 2022

  28. [28]

    Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2012. Frama-C - A Software Analysis Perspective. InProceedings of the 10th International Conference on Software Engineering and Formal Methods (SEFM 2012) (Lecture Notes in Computer Science, Vol. 7504), George Eleftherakis, Mike Hinchey, and Mike Holc...

    work page doi:10.1007/978-3-642-33826-7_16 2012

  29. [29]

    Haowei Deng, Runzhou Tao, Yuxiang Peng, and Xiaodi Wu. 2024. A Case for Synthesis of Recursive Quantum Unitary Programs.Proceedings of the ACM on Programming Languages8, POPL (2024), 1759–1788. doi:10.1145/3632901

    work page doi:10.1145/3632901 2024

  30. [30]

    1637.Discours de la méthode

    René Descartes. 1637.Discours de la méthode. Jan Maire – Vrin 1987

    1987

  31. [31]

    Bryce S DeWitt. 1970. Quantum mechanics and reality.Physics today23, 9 (1970), 30–35. doi:10.1063/1.3022331

    work page doi:10.1063/1.3022331 1970

  32. [32]

    Paul Adrien Maurice Dirac. 1939. A new notation for quantum mechanics. InMathematical proceedings of the Cambridge philosophical society, Vol. 35. Cambridge University Press, 416–418. doi:10.1017/S0305004100021162

    work page doi:10.1017/s0305004100021162 1939

  33. [33]

    Relative state

    Hugh Everett III. 1957. “Relative state” formulation of quantum mechanics.Reviews of modern physics29, 3 (1957), 454. doi:10.1103/RevModPhys.29.454

    work page doi:10.1103/revmodphys.29.454 1957

  34. [34]

    Wang Fang and Mingsheng Ying. 2024. Symbolic execution for quantum error correction programs.Proceedings of the ACM on Programming Languages8, PLDI (2024), 1040–1065. doi:10.1145/3656419

    work page doi:10.1145/3656419 2024

  35. [35]

    A Quantum Approximate Optimization Algorithm

    Edward Farhi, Jeffrey Goldstone, and Sam Gutmann. 2014.A Quantum Approximate Optimization Algorithm. Technical Report MIT-CTP/4610. MIT. doi:10.48550/arXiv.1411.4028

    work page internal anchor Pith review doi:10.48550/arxiv.1411.4028 2014

  36. [36]

    Yuan Feng and Mingsheng Ying. 2020. Quantum Hoare logic with classical variables.CoRRabs/2008.06812 (2020). arXiv:2008.06812 doi:10.1145/3456877

    work page doi:10.1145/3456877 2020

  37. [37]

    Richard Feynman. 1960. There’s Plenty of Room at the Bottom.Engineering and Science23 (1960), 79. https: //resolver.caltech.edu/CaltechES:23.5.1960Bottom

    1960

  38. [38]

    Jacques Garrigue and Takafumi Saikawa. 2023. Typed compositional quantum computation with lenses.arXiv preprint arXiv:2311.14347(2023). doi:10.48550/arXiv.2311.14347

    work page internal anchor Pith review doi:10.48550/arxiv.2311.14347 2023

  39. [39]

    Hairer, S

    Simon J. Gay, Rajagopal Nagarajan, and Nikolaos Papanikolaou. 2008. QMC: A Model Checker for Quantum Systems. InProceeding of the 20th International Conference on Computer Aided Verification (CA V 2008) (Lecture Notes in Computer Science, Vol. 5123), Aarti Gupta and Sharad Malik (Eds.). Springer, Princeton, NJ, USA, 543–547. doi:10.1007/978-3-540- 70545-1_51

    work page doi:10.1007/978-3-540- 2008

  40. [40]

    A Geller. [n. d.]. Introducing Quantum Intermediate Representation (QIR). 2020 September 23rd, 2020 [cited 2021 03/22/2021]

    2020

  41. [41]

    Iulia M Georgescu, Sahel Ashhab, and Franco Nori. 2014. Quantum Simulation.Reviews of Modern Physics86, 1 (2014),

    2014

  42. [42]

    doi:10.1103/RevModPhys.86.153

    work page doi:10.1103/revmodphys.86.153

  43. [43]

    Georges Gonthier. 2008. Formal Proof — the Four-Color Theorem.Notices of the AMS55, 11 (2008), 1382–1393. https://www.ams.org/notices/200811/index.html

    2008

  44. [44]

    Reliable evaluation of adversarial robustness with an ensemble of diverse parameter-free attacks

    Daniel Gottesman. 1997.Stabilizer codes and quantum error correction. Ph. D. Dissertation. Caltech. doi:10.48550/arXiv. quant-ph/9705052

    work page internal anchor Pith review doi:10.48550/arxiv 1997

  45. [45]

    Arun Govindankutty and Sudarshan K Srinivasan. 2026. Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits.arXiv preprint arXiv:2603.08762(2026). doi:10.48550/arXiv.2603.08762

    work page doi:10.48550/arxiv.2603.08762 2026

  46. [46]

    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. InProceedings of the ACM SIGPLAN Conference on Programming Language Design 26 Christophe Chareton, Jad Issa, Mathieu Nguyen, Nicolas Blanco, and Sébastien Bardin and Implementation, (PLDI’13), Hans-Juergen B...

    work page doi:10.1145/2491956.2462177 2013

  47. [47]

    Harrow, Avinatan Hassidim, and Seth Lloyd

    Aram W. Harrow, Avinatan Hassidim, and Seth Lloyd. 2009. Quantum Algorithm for Linear Systems of Equations. Physical Review Letters103 (Oct 2009), 150502. Issue 15. doi:10.1103/PhysRevLett.103.150502

    work page doi:10.1103/physrevlett.103.150502 2009

  48. [48]

    Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. 2021. A verified optimizer for Quantum circuits.Proc. ACM Program. Lang.5, POPL (2021), 1–29. doi:10.1145/3434318

    work page doi:10.1145/3434318 2021

  49. [49]

    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 Cezary Kaliszyk (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl,...

    work page doi:10.4230/lipics.itp.2021.21 2021

  50. [50]

    Xin Hong, Yuan Feng, Sanjiang Li, and Mingsheng Ying. 2022. Equivalence checking of dynamic quantum circuits. In Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design. 1–8. doi:10.1145/3508352.3549479

    work page doi:10.1145/3508352.3549479 2022

  51. [51]

    https://web.archive.org/web/20170417095446/http://www.emc.com/emc-plus/rsa-labs/historical/the-rsa- laboratories-secret-key-challenge.htm [n. d.]

    work page arXiv

  52. [52]

    Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, and Mingsheng Ying. 2025. Efficient Formal Verification of Quantum Error Correcting Programs.Proceedings of the ACM on Programming Languages9, PLDI (2025), 1068–1093. doi:10.1145/3729293

    work page doi:10.1145/3729293 2025

  53. [54]

    Shelby Kimmel, Guang Hao Low, and Theodore J Yoder. 2015. Robust calibration of a universal single-qubit gate set via robust phase estimation.Physical Review A92, 6 (2015), 062315. doi:10.1103/PhysRevA.92.062315

    work page doi:10.1103/physreva.92.062315 2015

  54. [55]

    Aleks Kissinger and John van de Wetering. 2018. PyZX. https://github.com/Quantomatic/pyzx

    2018

  55. [56]

    A Yu Kitaev. 1995. Quantum measurements and the Abelian stabilizer problem. (1995). doi:10.48550/arXiv.quant- ph/9511026 Available online asarXiv:quant-ph/9511026

    work page doi:10.48550/arxiv.quant- 1995

  56. [57]

    A Yu Kitaev. 2003. Fault-tolerant quantum computation by anyons.Annals of physics303, 1 (2003), 2–30. doi:10.1016/ S0003-4916(02)00018-0

    2003

  57. [58]

    Erwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2010. seL4: formal verification of an operating-system kernel.Commun. ACM53, 6 (2010), 107–115. doi:10.1145/1629575.1629596

    work page doi:10.1145/1629575.1629596 2010

  58. [59]

    1996.Conventions for quantum pseudocode

    Emmanuel Knill. 1996.Conventions for quantum pseudocode. Technical Report. Los Alamos National Lab., NM (United States)

    1996

  59. [60]

    Emanuel Knill. 2004. Fault-tolerant postselected quantum computation: Schemes.arXiv preprint quant-ph/0402171 (2004). doi:10.48550/arXiv.quant-ph/0402171

    work page doi:10.48550/arxiv.quant-ph/0402171 2004

  60. [61]

    2012.The CompCert verified compiler

    Xavier Leroy et al. 2012.The CompCert verified compiler. Documentation and user’s manual. INRIA Paris-Rocquencourt

    2012

  61. [62]

    Marco Lewis, Paolo Zuliani, and Sadegh Soudjani. 2024. Automated Verification of Silq Quantum Programs using SMT Solvers. In2024 IEEE International Conference on Quantum Software (QSW). 125–134. doi:10.1109/QSW62656.2024.00027

    work page doi:10.1109/qsw62656.2024.00027 2024

  62. [63]

    Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. 2024. Qafny: A Quantum-Program Verifier. In38th European Conference on Object-Oriented Programming (ECOOP 2024). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 24–1. doi:10.4230/LIPIcs.ECOOP.2024.24

    work page doi:10.4230/lipics.ecoop.2024.24 2024

  63. [64]

    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. InComputer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham, 187–207. doi:10.1007/978-3-030-25543-5_12

    work page doi:10.1007/978-3-030-25543-5_12 2019

  64. [65]

    Jingyi Mei, Tim Coopmans, Marcello Bonsangue, and Alfons Laarman. 2024. Equivalence checking of quantum circuits by model counting. InInternational Joint Conference on Automated Reasoning. Springer, 401–421. doi:10.1007/978-3- 031-63501-4_21

    work page doi:10.1007/978-3- 2024

  65. [66]

    Mathieu Nguyen, Christophe Chareton, and Jad Issa. 2026. HQbricks, Reproduction Package for Article ‘Hybrid Path-Sums for Hybrid Quantum Programs’. Zenodo. doi:10.5281/zenodo.19080602

    work page doi:10.5281/zenodo.19080602 2026

  66. [67]

    Nielsen and Isaac Chuang

    Michael A. Nielsen and Isaac Chuang. 2002.Quantum computation and quantum information. Cambridge University Press, Cambridge, United Kingdom

    2002

  67. [68]

    Anouk Paradis, Benjamin Bichsel, Samuel Steffen, and Martin Vechev. 2021. Unqomp: synthesizing uncomputation in Quantum circuits. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Association for Computing Machinery, New York, NY, USA, 222–236. doi:10.1145/3453483.3454040

    work page doi:10.1145/3453483.3454040 2021

  68. [69]

    Anouk Paradis, Benjamin Bichsel, and Martin Vechev. 2024. Reqomp: Space-constrained Uncomputation for Quantum Circuits.Quantum8 (2024), 1258. doi:10.22331/q-2024-02-19-1258 Hybrid Path-Sums for Hybrid Quantum Programs 27

    work page doi:10.22331/q-2024-02-19-1258 2024

  69. [70]

    Tom Peham, Lukas Burgholzer, and Robert Wille. 2022. Equivalence checking of quantum circuits with the ZX-calculus. IEEE Journal on Emerging and Selected Topics in Circuits and Systems12, 3 (2022), 662–675. doi:10.1109/JETCAS.2022. 3202204

    work page doi:10.1109/jetcas.2022 2022

  70. [71]

    Simon Perdrix. 2008. Quantum entanglement analysis based on abstract interpretation. InInternational Static Analysis Symposium. Springer, 270–282. doi:10.1007/978-3-540-69166-2_18

    work page doi:10.1007/978-3-540-69166-2_18 2008

  71. [72]

    Alberto Peruzzo, Jarrod McClean, Peter Shadbolt, Man-Hong Yung, Xiao-Qi Zhou, Peter J Love, Alán Aspuru-Guzik, and Jeremy L O’brien. 2014. A variational eigenvalue solver on a photonic quantum processor.Nature communications 5, 1 (2014), 4213. doi:10.1038/ncomms5213

    work page doi:10.1038/ncomms5213 2014

  72. [73]

    2018.Formally Verified Quantum Programming

    Robert Rand. 2018.Formally Verified Quantum Programming. Ph. D. Dissertation. University of Pennsylvania

    2018

  73. [74]

    Robert Rand, Kesha Hietala, and Michael Hicks. 2019. Formal Verification vs. Quantum Uncertainty. In3rd Summit on Advances in Programming Languages (SNAPL 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Providence, RI, USA. doi:10.4230/LIPIcs.SNAPL.2019.12

    work page doi:10.4230/lipics.snapl.2019.12 2019

  74. [75]

    Robert Raussendorf, Daniel E Browne, and Hans J Briegel. 2003. Measurement-based quantum computation on cluster states.Physical review A68, 2 (2003), 022312. doi:10.1103/PhysRevA.68.022312

    work page doi:10.1103/physreva.68.022312 2003

  75. [76]

    Jérome Ricciardi, Sébastien Bardin, Christophe Chareton, and Benoît Valiron. 2025. Quantum Circuit Equivalence Checking: A Tractable Bridge From Unitary to Hybrid Circuits. In3rd International Workshop on Services and Quantum Software. doi:10.48550/arXiv.2511.22523

    work page doi:10.48550/arxiv.2511.22523 2025

  76. [77]

    Joschka Roffe. 2019. Quantum error correction: an introductory guide.Contemporary Physics60, 3 (2019), 226–245. doi:10.1080/00107514.2019.1667078

    work page doi:10.1080/00107514.2019.1667078 2019

  77. [78]

    Neil J. Ross. 2015.Algebraic and Logical Methods in Quantum Computation. Ph. D. Dissertation. Dalhousie University. doi:10.48550/arXiv.1510.02198 Available asarxiv:1510.02198

    work page doi:10.48550/arxiv.1510.02198 2015

  78. [79]

    Raphael Seidel, Sebastian Bock, René Zander, Matic Petrič, Niklas Steinmann, Nikolay Tcholtchev, and Manfred Hauswirth. 2024. Qrisp: A framework for compilable high-level programming of gate-based quantum computers. arXiv preprint arXiv:2406.14792(2024). doi:10.48550/arXiv.2406.14792

    work page doi:10.48550/arxiv.2406.14792 2024

  79. [80]

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

    work page doi:10.1017/s0960129504004256 2004

  80. [81]

    Peter Selinger and Benoît Valiron. 2005. A Lambda Calculus for Quantum Computation with Classical Control. In Typed Lambda Calculi and Applications, Paweł Urzyczyn (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 354–368. doi:doi:10.1017/S0960129506005238

    work page doi:10.1017/s0960129506005238 2005

Showing first 80 references.