pith. sign in

arxiv: 2412.09869 · v4 · submitted 2024-12-13 · 💻 cs.PL · cs.LO· quant-ph

A Practical Quantum Hoare Logic with Classical Variables, I

Mingsheng Ying This is my paper

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

classification 💻 cs.PL cs.LOquant-ph
keywords quantum Hoare logicclassical variablesquantum arraysparameterized quantum gatesprogram verificationproof systemquantum measurementsHoare logic
0
0 comments X

The pith

A Hoare-style logic for quantum programs with classical variables uses paired classical-quantum specifications and a new measurement rule to require only minimal changes to classical Hoare logic.

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

The paper develops a Hoare-style logic for reasoning about quantum programs that include classical variables along with quantum arrays and parameterized quantum gates. Preconditions and postconditions are given as a pair consisting of a classical first-order logical formula and a quantum predicate formula. By introducing a novel proof rule for quantum measurements, the resulting proof system needs only minimal modifications to classical Hoare logic and combines directly with classical first-order logic. This makes the verification techniques accessible to those already familiar with classical methods and allows existing classical verification tools to be adapted more readily.

Core claim

The paper claims that preconditions and postconditions specified as a pair of a classical first-order logical formula and a quantum predicate formula, together with a novel formulation of the proof rule for quantum measurements, permit a proof system for quantum programs with classical variables, quantum arrays, and parameterized quantum gates that requires only minimal modifications to classical Hoare logic and can be effectively combined with classical first-order logic.

What carries the argument

The paired classical first-order formula and quantum predicate for preconditions and postconditions, together with the novel proof rule for quantum measurements.

If this is right

  • The logic applies directly to quantum programs that incorporate quantum arrays and parameterized quantum gates.
  • Correctness specifications align more closely with a programmer's intuitive understanding of quantum-classical interactions.
  • The proof system combines effectively with classical first-order logic to verify quantum programs with classical variables.
  • Existing tools for verifying classical programs can be adapted for quantum program verification.
  • The learning curve for quantum program verification is reduced for those already familiar with classical techniques.

Where Pith is reading between the lines

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

  • Verification of hybrid quantum-classical algorithms could reuse large parts of existing classical proof infrastructure.
  • The paired specification format may simplify integration of quantum verification into mainstream software development environments.
  • Further work could test whether the same paired-spec approach extends to quantum programs with classical control flow beyond arrays and parameterized gates.

Load-bearing premise

The novel formulation of the proof rule for quantum measurements together with the paired classical-quantum specifications permits effective and sound combination with classical first-order logic for verification.

What would settle it

A concrete quantum program containing classical variables, a quantum array, a parameterized gate, and a measurement, together with a claimed correctness pair that the logic either cannot prove when true or incorrectly proves when false, would show the approach fails to deliver sound and practical verification.

read the original abstract

In this paper, we present a Hoare-style logic for reasoning about quantum programs with classical variables. Our approach offers several improvements over previous work: (1) Enhanced expressivity of the programming language: Our logic applies to quantum programs with classical variables that incorporate quantum arrays and parameterised quantum gates, which have not been addressed in previous research on quantum Hoare logic, either with or without classical variables. (2) Intuitive correctness specifications: In our logic, preconditions and postconditions for quantum programs with classical variables are specified as a pair consisting of a classical first-order logical formula and a quantum predicate formula (possibly parameterised by classical variables). These specifications offer greater clarity and align more closely with the programmer's intuitive understanding of quantum and classical interactions. (3) Simplified proof system: By introducing a novel idea in formulating a proof rule for reasoning about quantum measurements, along with (2), we develop a proof system for quantum programs that requires only minimal modifications to classical Hoare logic. Furthermore, this proof system can be effectively and conveniently combined with classical first-order logic to verify quantum programs with classical variables. As a result, the learning curve for quantum program verification techniques is significantly reduced for those already familiar with classical program verification techniques, and existing tools for verifying classical programs can be more easily adapted for quantum program verification.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 2 minor

Summary. The paper presents a Hoare-style logic for quantum programs with classical variables. It claims three improvements: (1) support for quantum arrays and parameterized gates (not handled in prior quantum Hoare logics), (2) correctness specifications given as pairs of a classical first-order formula and a (possibly parameterized) quantum predicate, and (3) a proof system obtained by only minimal modifications to classical Hoare logic, achieved via a novel measurement rule that permits effective combination with classical FOL.

Significance. If the central claims hold, the work would lower the barrier to quantum program verification by allowing reuse of classical verification expertise and tools, while extending expressivity to previously unaddressed language features.

major comments (2)
  1. [Proof rules for quantum measurements (central to § on the proof system)] The novel measurement rule (described in the proof-system development) is load-bearing for claim (3). The abstract asserts that the paired classical-FOL + quantum-predicate specifications plus this rule require “only minimal modifications” and allow “effective and convenient” combination with classical first-order logic, yet no derivation, side-condition analysis, or soundness argument is supplied showing that the rule avoids introducing quantum-specific axioms, non-classical reasoning steps, or additional constraints on the classical formula when classical variables receive probabilistic information from measurement.
  2. [Introduction and related-work discussion] Expressivity claim (1) asserts that quantum arrays and parameterized gates “have not been addressed in previous research,” but the manuscript supplies neither concrete program examples using these features nor a precise comparison (e.g., against the languages treated in cited prior quantum Hoare logics) that would confirm the extension is both novel and handled by the new logic without further changes to the assertion language or rules.
minor comments (2)
  1. The title indicates this is Part I; the manuscript should clarify the division of material between parts and whether soundness proofs appear in Part II.
  2. Notation for the paired assertions (classical formula, quantum predicate) should be introduced with an explicit example early in the text to make the “intuitive” claim concrete.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review. The two major comments identify areas where the manuscript would benefit from additional detail and substantiation. We address each point below and commit to revisions that strengthen the paper without altering its core claims.

read point-by-point responses

  1. Referee: [Proof rules for quantum measurements (central to § on the proof system)] The novel measurement rule (described in the proof-system development) is load-bearing for claim (3). The abstract asserts that the paired classical-FOL + quantum-predicate specifications plus this rule require “only minimal modifications” and allow “effective and convenient” combination with classical first-order logic, yet no derivation, side-condition analysis, or soundness argument is supplied showing that the rule avoids introducing quantum-specific axioms, non-classical reasoning steps, or additional constraints on the classical formula when classical variables receive probabilistic information from measurement.

    Authors: We agree that the current manuscript presents the novel measurement rule but does not supply the requested derivation, side-condition analysis, or explicit soundness argument. This is a genuine gap in the exposition. In the revised version we will add a dedicated subsection that derives the rule from the underlying semantics, states and justifies all side conditions, and proves soundness. The proof will explicitly demonstrate that the rule permits direct combination with classical FOL without introducing quantum-specific axioms, non-classical reasoning steps, or extra constraints on the classical formula beyond those already present in standard probabilistic Hoare logic. revision: yes

  2. Referee: [Introduction and related-work discussion] Expressivity claim (1) asserts that quantum arrays and parameterized gates “have not been addressed in previous research,” but the manuscript supplies neither concrete program examples using these features nor a precise comparison (e.g., against the languages treated in cited prior quantum Hoare logics) that would confirm the extension is both novel and handled by the new logic without further changes to the assertion language or rules.

    Authors: We accept that the manuscript would be stronger with concrete examples and a precise comparison. While the abstract and introduction assert the claim, the text does not include worked program examples that exercise quantum arrays and parameterized gates, nor a side-by-side comparison against the languages of the cited prior logics. In revision we will add (i) at least two small but non-trivial program fragments that use these features and (ii) an expanded related-work paragraph (or table) that identifies the precise language fragments treated in each cited work and confirms that the new assertion language and rules accommodate the additional constructs without further extension. revision: yes

Circularity Check

0 steps flagged

No circularity; new logic presented as independent extension of classical Hoare logic

full rationale

The paper presents a Hoare-style logic for quantum programs with classical variables, quantum arrays, and parameterized gates. It claims a novel measurement rule plus paired classical-FOL + quantum-predicate specs yields a proof system via only minimal modifications to classical Hoare logic. No self-definitional steps, fitted inputs renamed as predictions, or load-bearing self-citation chains appear in the claims. The derivation is framed as a fresh formulation that remains self-contained against the external benchmark of classical Hoare logic; the central result does not reduce to its own inputs by construction. This is the expected honest non-finding for a theoretical logic paper whose soundness argument is not shown to collapse into prior self-work.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract provides no details on free parameters, axioms or invented entities; full paper would be needed to identify any such elements in the logic definition.

pith-pipeline@v0.9.0 · 5763 in / 1136 out tokens · 42722 ms · 2026-05-23T07:41:46.725734+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

72 extracted references · 72 canonical work pages

  1. [1]

    K. R. Apt, F. S. de Boer and E. -R. Olderog, Verification of Sequential and Concurrent Programs, Springer, London 2009

    work page 2009

  2. [2]

    Barthe, J

    G. Barthe, J. Hsu, M. S. Ying, N. K. Yu and L. Zhou, Relational proofs for quantum programs, Proceedings of ACM Programming Languages 4(2020) POPL: art. 21:1-29

    work page 2020

  3. [3]

    Bauer-Marquart, S

    F. Bauer-Marquart, S. Leue and C. Schilling, symQV: automated sym- bolic verification of quantum programs, Proceedings of the 25th Inter- national Symposium on Formal Methods (FM) , 2023, pp. 181-198

    work page 2023

  4. [4]

    Biamonte, P

    J. Biamonte, P. Wittek, N. Pancotti, P. Rebentrost, N. Wiebe and S. Lloyd, Quantum machine learning, Nature 549(2017) 195-202

    work page 2017

  5. [5]

    Birkhoff and J

    G. Birkhoff and J. von Neumann, The logic of quantum mechanics, Annals of Mathematics , 37(1936) 823-843

    work page 1936

  6. [6]

    Carette, G

    J. Carette, G. Ortiz and A. Sabry, Symbolic execution of Hadamard- Toffoli quantum circuits, Proceedings of the 2023 ACM International Workshop on Partial Evaluation and Program Manipulation (PEPM) , pp. 14-26

    work page 2023

  7. [7]

    Cerezo, A

    M. Cerezo, A. Arrasmith, R. Babbush, S. C. Benjamin, S. Endo, K. Fujii, J. R. McClean, K. Mitarai, X. Yuan, L. Cincio and P. J. Coles, Variational quantum algorithms, Nature Reviews Physics 3(2021) 625- 644

    work page 2021

  8. [8]

    Chadha, P

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

    work page 2006

  9. [9]

    Chareton, S

    C. Chareton, S. Bardin, F. Bobot, V. Perrelle and B. Valiron, An au- tomated deductive verification framework for circuit-building quantum programs, Proceedings of the 30th European Symposium on Program- ming (ESOP), 2021, pp. 148-177. 41

    work page 2021

  10. [10]

    Chareton, D

    C. Chareton, D. Lee, B. Valiron, R. Vilmart, S. Bardin and Z. W. Xu, Formal methods for quantum algorithms, in: Handbook of Formal Anal- ysis and Verification in Cryptography, CRC Press 2023, pp. 319-422

    work page 2023

  11. [11]

    Cross, A

    A. Cross, A. Javadi-Abhari, T. Alexander, N. De Beaudrap, L. S. Bishop, S. Heidel, C. A. Ryan, P. Sivarajah, J. Smolin, J. M. Gambetta and B. R. Johnson, OpenQASM 3: a broader and deeper quantum as- sembly language, ACM Transactions on Quantum Computing 3(2022) 12:1-50

    work page 2022

  12. [12]

    Y. X. Deng and Y. Feng, Formal semantics of a classical-quantum lan- guage, Theoretical Computer Science 913(2022) 73-93

    work page 2022

  13. [13]

    Y. X. Deng, H. L. Wu and M. Xu, Local reasoning about probabilis- tic behaviour for classical–quantum programs, Proceedings of the 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2024, pp. 163-184

    work page 2024

  14. [14]

    D’Hondt and P

    E. D’Hondt and P. Panangaden, Quantum weakest preconditions, Math- ematical Structures in Computer Science , 16(2006)429-451

    work page 2006

  15. [15]

    C. M. Do, T. Takagi and K. Ogata, Automated quantum program veri- fication in probabilistic dynamic quantum logic, The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryp- tographic Protocols, 2023

    work page 2023

  16. [16]

    Fang and M

    W. Fang and M. S. Ying, Symbolic execution for quantum error correc- tion programs, Proceedings of ACM Programming Languages 8(2024) PLDI: 1040-1065

    work page 2024

  17. [17]

    W. Fang, M. S. Ying and X. D. Wu, Differentiable quantum program- ming with unbounded loops, ACM Transactions on Software Engineer- ing and Methodology 33(2024) 19:1-63

    work page 2024

  18. [18]

    Y. Feng, R. Y. Duan, Z. F. Ji and M. S. Ying, Proof rules for the correctness of quantum programs, Theoretical Computer Science , 386 (2007), 151-166

    work page 2007

  19. [19]

    Y. Feng, S. J. Li and M. S. Ying, Verification of distributed quantum programs, ACM Transactions on Computational Logic 23(2022), art. 19:1-40. 42

    work page 2022

  20. [20]

    Feng and Y

    Y. Feng and Y. T. Xu, Verification of nondeterministic quantum pro- grams, Proceedings of the 28th ACM International Conference on Ar- chitectural Support for Programming Languages and Operating Systems (ASPLOS), 2023, pp. 789-805

    work page 2023

  21. [21]

    Feng and M

    Y. Feng and M. S. Ying, Quantum Hoare logic with classical variables, ACM Transactions on Quantum Computing 2(2021) art. 16, pp. 1-43

    work page 2021

  22. [22]

    Y. Feng, L. Zhou and Y. Xu, Refinement calculus of quantum programs with projective assertions, arXiv 2311.14215 (2023)

    work page arXiv 2023

  23. [23]

    D. J. Foulis and M. K. Bennett, Effect algebras and unsharp quantum logics, Foundations of Physics 24(1994) 1331-1352

    work page 1994

  24. [24]

    J. D. Hartog and E. P. de Vink, Verifying probabilistic programs using a Hoare like logic, International Journal of Foundations of Computer Science, 13 (2003)315-340

    work page 2003

  25. [25]

    Hietala, A Verified Software Toolchain for Quantum Programming , PhD Thesis, University of Maryland, 2022

    K. Hietala, A Verified Software Toolchain for Quantum Programming , PhD Thesis, University of Maryland, 2022

    work page 2022

  26. [26]

    Hietala, R

    K. Hietala, R. Rand, S. H. Hung, X. D. Wu and M. Hicks, A verified op- timizer for quantum circuits, Proceedings of the ACM on Programming Languages 5(2021): POPL, art. no. 31:1-29

    work page 2021

  27. [27]

    Jorrand and S

    P. Jorrand and S. Perdrix, Abstract interpretation techniques for quan- tum computation, in: I. Mackie, S. Gay (Eds.), Semantic Techniques in Quantum Computation, Cambridge University Press, 2010, pp. 206-234

    work page 2010

  28. [28]

    Kakutani, A logic for formal verification of quantum programs, In: Proceedings of the 13th Asian Computing Science Conference (ASIAN) , Springer LNCS 5913, 2009, pp

    Y. Kakutani, A logic for formal verification of quantum programs, In: Proceedings of the 13th Asian Computing Science Conference (ASIAN) , Springer LNCS 5913, 2009, pp. 79-93

    work page 2009

  29. [29]

    X. -B. Le, S. -W. Lin, J. Sun and D. San´ an, A quantum interpreta- tion of separating conjunction for local reasoning of quantum programs based on separation logic, Proceedings of ACM Programming Languages 6(2022) POPL: 1-27

    work page 2022

  30. [30]

    Lewis, S

    M. Lewis, S. Soudjani and P. Zuliani, Formal verification of quantum programs: theory, tools and challenges, ACM Transactions on Quantum Computing 5(2024) art. 1:1-35. 43

    work page 2024

  31. [31]

    L. Y. Li, M. W. Zhu, R. Cleaveland, A. Nicolellis, Y. Lee, L. Chang and X. D. Wu, Qafny: a quantum-program verifier, arXiv: 2211.06411 (2022)

    work page arXiv 2022

  32. [32]

    L. Y. Li, F. Voichick, K. Hietala, Y. X. Peng, X. D. Wu and M. Hicks, Verified compilation of quantum oracles, Proceedings of the ACM on Programming Languages 6(OOPSLA2) 589-615

    work page

  33. [33]

    Y. J. Li and D. Unruh, Quantum relational Hoare logic with expecta- tions, ICALP 2021. art. 136: 1-20

    work page 2021

  34. [34]

    J. Y. Liu, B. H. Zhan, S. L. Wang, S. G. Ying, T. Liu, Y. J. Li, M. S. Ying and N. J. Zhan, Formal verification of quantum algorithms using quantum Hoare logic, Proceedings of the 31st International Conference on Computer Aided Verification (CAV), 2019, pp. 187-207

    work page 2019

  35. [35]

    Loeckx and K

    J. Loeckx and K. Sieber, Foundations of Program Verification , John Wiley & Sons, Chichester 1987

    work page 1987

  36. [36]

    Mateus and A

    P. Mateus and A. Sernadas, Weakly complete axiomatization of ex- ogenous quantum propositional logic, Information and Computation 204(2006) 771-794

    work page 2006

  37. [37]

    Meuli, M

    G. Meuli, M. Soeken, M. Roetteler and T. H¨ aner, Enabling accuracy- aware Quantum compilers using symbolic resource estimation, Proceed- ings of the ACM on Programming Languages 4(2020) OOPSLA: 130.1- 26

    work page 2020

  38. [38]

    M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000

    work page 2000

  39. [39]

    Peduri, I

    A. Peduri, I. Schaefer and M. Walter, QbC: quantum correctness by construction, arXiv:2307.15641 (2023)

    work page arXiv 2023

  40. [40]

    Y. X. Peng, Theoretical and Practical High-Assurance Software Tools for Quantum Applications , PhD Thesis, University of Maryland, 2024

    work page 2024

  41. [41]

    Y. X. Peng, K. Hietala, R. Z. Tao, L. Y. Li, R. Rand, M Hicks and X. D. Wu, A formally certified end-to-end implementation of Shor’s factorization algorithm, Proceedings of the National Academy of Sciences 120(2023) e2218775120. 44

    work page 2023

  42. [42]

    Perdrix, Quantum entanglement analysis based on abstract interpre- tation, in: Proceedings of the 2008 International Static Analysis Sympo- sium (SAS), pp

    S. Perdrix, Quantum entanglement analysis based on abstract interpre- tation, in: Proceedings of the 2008 International Static Analysis Sympo- sium (SAS), pp. 270-282

    work page 2008

  43. [43]

    Rand, Formally Verified Quantum Programming, PhD Thesis, Uni- versity of Pennsylvania, 2018

    R. Rand, Formally Verified Quantum Programming, PhD Thesis, Uni- versity of Pennsylvania, 2018

    work page 2018

  44. [44]

    Selinger, Towards a quantum programming language, Mathematical Structures in Computer Science 14(2004) 527-586

    P. Selinger, Towards a quantum programming language, Mathematical Structures in Computer Science 14(2004) 527-586

    work page 2004

  45. [45]

    Y. N. Shi, Compilation, Optimization and Verification of Near-Term Quantum Computing, PhD Thesis, University of Chicago, 2020

    work page 2020

  46. [46]

    Singhal, R

    K. Singhal, R. Rand and M. Amy, Beyond separation: toward a speci- fication language for modular reasoning about quantum programs, Pro- gramming Languages for Quantum Computing (PLanQC) , 2022

    work page 2022

  47. [47]

    Svore, A

    K. Svore, A. Geller, M. Troyer, J. Azariah, C. Granade, B. Heim, V. Kliuchnikov, M. Mykhailova, A. Paz and M. Roetteler, Q# enabling scalable quantum computing and development with a high-level domain- specific language, Proceedings of the Real World Domain Specific Lan- guages Workshop, 2018, pp. 7:1-10

    work page 2018

  48. [48]

    Takagi, C

    T. Takagi, C. M. Do and K. Ogata, Automated quantum program veri- fication in dynamic quantum logic, Proceedings of the 5th International Workshop on Dynamic Logic , 2023, pp.68-84

    work page 2023

  49. [49]

    R. Z. Tao, Formal Verifcation of Quantum Software , PhD Thesis, Uni- versity of Columbia, 2024

    work page 2024

  50. [50]

    R. Z. Tao, Y. N. Shi, J. Yao, X. Li, A. Javadi-Abhari, A. W. Cross, F. T. Chong, R. H. Gu, Giallar: push-button verification for the qiskit quantum compiler, Proceedings of the 43rd ACM International Confer- ence on Programming Language Design and Implementation , 2022, pp. 641-656

    work page 2022

  51. [51]

    Unruh, Quantum Hoare logic with ghost variables, Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2019

    D. Unruh, Quantum Hoare logic with ghost variables, Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2019. 45

    work page 2019

  52. [52]

    Unruh, Quantum relational Hoare logic, Proceedings of ACM Pro- gramming Languages 3(2019) POPL: art

    D. Unruh, Quantum relational Hoare logic, Proceedings of ACM Pro- gramming Languages 3(2019) POPL: art. 33:1-31

    work page 2019

  53. [53]

    Valiron, On Quantum Programming Languages , Habilitation Disser- tation, University of Paris - Saclay, 2024

    B. Valiron, On Quantum Programming Languages , Habilitation Disser- tation, University of Paris - Saclay, 2024

    work page 2024

  54. [54]

    von Neumann, On infinite direct products, Compositio Mathematica, tome 6(1939) 1-77

    J. von Neumann, On infinite direct products, Compositio Mathematica, tome 6(1939) 1-77

    work page 1939

  55. [55]

    Z. Xu, M. S. Ying and B. Valiron, Reasoning about recursive quantum programs, arXiv:2107.11679 (2021)

    work page arXiv 2021

  56. [56]

    P. Yan, H. R. Jiang and N. K. Yu, On incorrectness logic for quan- tum programs, Proceedings of ACM Programming Languages 6(2022) OOPSLA: 1-28

    work page 2022

  57. [57]

    P. Yan, H. R. Jiang and N. K. Yu, Approximate relational reasoning for quantum programs, Proceedings of the 36th International Conference on Computer Aided Verification (CAV), 2024, pp. 495-519

    work page 2024

  58. [58]

    M. S. Ying, Floyd-Hoare logic for quantum programs, ACM Transac- tions on Programming Languages and Systems 33(2011) art. no: 19, pp. 1-49

    work page 2011

  59. [59]

    M. S. Ying, Toward automatic verification of quantum programs,Formal Aspects of Computing 31(2019) 3-25

    work page 2019

  60. [60]

    M. S. Ying, Birkhoff-von Neumann quantum logic as an assertion lan- guage for quantum programs, arXiv 2205.01959 (2022)

    work page arXiv 2022

  61. [61]

    M. S. Ying, Foundations of Quantum Programming (Second Edition), Morgan Kauffman, 2024

    work page 2024

  62. [62]

    M. S. Ying, A practical quantum Hoare logic with classical variables, II, in preparation

    work page

  63. [63]

    M. S. Ying and Y. Feng, A flowchart language for quantum program- ming, IEEE Transactions on Software Engineering 37(2011) 466-485

    work page 2011

  64. [64]

    M. S. Ying and Z. C. Zhang, Quantum recursive programming with quantum case statements, arXiv 2311.01725 (2023). 46

    work page arXiv 2023

  65. [65]

    M. S. Ying and Z. C. Zhang, Verification of recursively defined quantum circuits, arXiv 2404.05934 (2024)

    work page arXiv 2024

  66. [66]

    M. S. Ying, L. Zhou and Y. J. Li, Reasoning about parallel quantum programs, arXiv: 1810.11334 (2018)

    work page arXiv 2018

  67. [67]

    N. K. Yu, Quantum temporal logic and reachability problems of matrix semigroups, Information and Computation 300(2024) 105197

    work page 2024

  68. [68]

    N. K. Yu, J. Palsberg, Quantum abstract interpretation, in: Proceedings of the 42nd ACM International Conference on Programming Language Design and Implementation (PLDI) , 2021, pp. 542-558

    work page 2021

  69. [69]

    L. Zhou, G. Barthe, J. Hsu, M. S. Ying and N. K. Yu, A quantum interpretation of bunched logic & quantum separation logic, LICS 2021: 1-14

    work page 2021

  70. [70]

    L. Zhou, G. Barthe, P. -Y. Strub, J. Y. Liu and M. S. Ying, CoqQ: foundational verification of quantum programs, Proceedings of ACM Programming Languages 7(2023) POPL: 833-865

    work page 2023

  71. [71]

    L. Zhou, N. K. Yu and M. S. Ying, An applied quantum Hoare logic, Proceedings of the 40th ACM Conference on Programming Language Design and Implementation (PLDI) , 2019, pp. 1149-1162

    work page 2019

  72. [72]

    :WD” stand for “is well-defined

    S. P. Zhu, S. -H. Hung, S. Chakrabarti and X. D. Wu, On the princi- ples of differentiable quantum programming languages, Proceedings of the 41st ACM Conference on Programming Language Design and Im- plementation (PLDI), 2020, pp. 272-285. Appendix A. Appendix: Deferred Proofs Appendix A.1. Proof of Lemma 4.2 We prove the substitution lemma by induction o...

    work page 2020