Pith. sign in

REVIEW 4 minor 40 references

A machine-checked theory of complex Hilbert spaces and bounded operators is presented in full, with proofs verified in the Isabelle/HOL proof assistant.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-03 18:15 UTC pith:PY2VCEP5

load-bearing objection Solid, machine-checked library paper; the formal content is the contribution and it checks out.

arxiv 2512.05878 v2 pith:PY2VCEP5 submitted 2025-12-05 cs.LO

Complex Bounded Operators in Isabelle/HOL

Dominique Unruh , Jos\'e Manuel Rodr\'iguez Caballero This is my paper
classification cs.LO MSC 03B3546C0547A0568V20
keywords bounded operatorsHilbert spacesIsabelle/HOLformal verificationfunctional analysisadjointsLoewner orderquantum programming
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

This paper presents a large formalized library that develops complex functional analysis from first principles: complex vector spaces, inner product spaces, Hilbert spaces, and the type of bounded linear operators (cblinfun). The central claim is that the standard toolkit of operator theory—adjoints, unitaries, projectors, the Riesz representation theorem, the BLT extension theorem, the Banach-Steinhaus theorem, the Loewner order, and the ℓ2 Hilbert space—can be stated and proved in a machine-checked way, including infinite-dimensional cases. The authors' motivation is that quantum-program verification often needs infinite-dimensional Hilbert spaces, where informal papers frequently gloss over topological subtleties such as which topology is used for infinite sums. If correct, the library gives researchers a verified foundation to build on instead of re-deriving or hand-waving these results.

Core claim

The central discovery is that the whole standard toolkit of complex functional analysis can be formalized in higher-order logic and machine-checked: bounded linear operators as a first-class type, adjoints, Riesz representation, extension of bounded operators from dense subspaces, uniform boundedness, orthogonal projections characterized as self-adjoint idempotents, the Loewner order, and the ℓ2 space of square-summable functions. The type cblinfun makes boundedness part of the type, so operators automatically form normed and Banach spaces, and many theorems can be stated without side conditions. Infinite-dimensional phenomena are handled explicitly—topologies for infinite sums, closed subsp

What carries the argument

The central object is the type cblinfun, the type of bounded linear operators between complex normed vector spaces, defined as those functions satisfying the predicate bounded_clinear. Around it, the machinery consists of type classes for complex vector spaces, inner product spaces, and Hilbert spaces; the conjugate-space construction that converts antilinear maps to linear ones; the one-dimensional-space isomorphism one_dim_iso; and for finite dimensions, an identification of operators with matrices that supports code generation.

Load-bearing premise

The library's correctness depends on the soundness of Isabelle/HOL itself and on the correctness of the existing libraries it imports; if any imported lemma or logic axiom is inconsistent, the verified status of the new theorems collapses.

What would settle it

A concrete check: ask Isabelle to verify the entire development from scratch and inspect for any 'sorry' or unproven assumption; then test the code-generation path by evaluating a concrete finite-dimensional operator expression and independently computing the same result with another tool—if the two disagree, the claimed correspondence fails.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Researchers formalizing quantum programs can now rely on verified infinite-dimensional Hilbert-space results instead of assuming finite-dimensional versions.
  • The BLT theorem gives a verified route to construct bounded operators from dense subspaces, a step that appears informally throughout functional analysis and quantum-mechanics papers.
  • The finite-dimensional matrix correspondence means concrete operator computations can be run and checked by Isabelle's code generator, not just reasoned about abstractly.
  • Projectors and the Loewner order provide a formal foundation for Birkhoff-von Neumann quantum logic inside a proof assistant.

Where Pith is reading between the lines

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

  • If this library is reused by later formalizations, the cost of new results in quantum cryptography and programming-language semantics drops substantially, since the functional-analysis infrastructure does not need to be re-proved from scratch.
  • The design choice to make cblinfun a type rather than a predicate suggests a general pattern: represent mathematically meaningful subclasses as dedicated types to unlock type-class automation, at the price of some loss of flexibility.
  • A natural next step would be to generalize the real/complex duplication noted by the authors, possibly via locales, so that theorems holding verbatim for both fields need only be proved once.
  • The explicit treatment of infinite-dimensional subtleties could serve as a checklist for informal papers: specifying operator topologies, trace-class assumptions, and closure conditions before claiming an operator equation.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

0 major / 4 minor

Summary. This paper presents the Isabelle/HOL formalization 'Complex_Bounded_Operators' (AFP entry, 2021), an extensive library for complex vector spaces, normed and Banach spaces, Hilbert spaces, and bounded operators (cblinfun). The main contributions are: the type of bounded operators with operator norm, adjoints, unitaries, isometries, partial isometries, projectors, the BLT extension theorem, Riesz representation, Banach–Steinhaus, the Loewner order on square operators, closed subspaces as a complete orthomodular lattice, the Hilbert space 'a ell2, a connection to finite-dimensional matrices via Jordan_Normal_Form, and code generation for finite-dimensional computations. The paper is written as an overview and user manual: definitions and the main theorems are stated with pointers to the Isabelle lemma names, while the proofs themselves live in the AFP development and are machine-checked.

Significance. If the described development is sound, this is a substantial contribution to formalized functional analysis and to the verification infrastructure for quantum programming languages. The paper reports 18,758 lines, 186 definitions, and 1,645 machine-checked lemmas. A particular strength is that the selection of results is driven by concrete applications (qrhl-tool, quantum registers, one-way-to-hiding, Kraus maps, tensor products), and the formalization is already used by several follow-up AFP entries. The library covers results that go beyond the real-vector-space material in HOL-Analysis, including antilinear and sesquilinear maps, conjugate spaces, the BLT theorem, Banach–Steinhaus for complex operators, and a workable Loewner order. The paper is honest about its main limitation: it is an overview of an AFP development rather than a self-contained proof paper, which is appropriate for this genre. The residual risks are the standard ones for any theorem-prover formalization: soundness of the Isabelle/HOL kernel and of the imported libraries. I found no evidence of internal inconsistency or unstated gaps in the claims as presented.

minor comments (4)
  1. [Section 4, 'Product spaces (continued)'] The text says 'In Section 14, we showed that the product of two complex vector spaces is a complex vector space.' There is no Section 14; the relevant results appear in Section 3. Please correct the cross-reference.
  2. [Section 9, code generation for matrices] The sentence 'This is important because the type complex vec of JNF-matrices contains matrices of all sizes in a single type' refers to matrices, but the type mentioned is complex vec (JNF vectors). It should be 'complex mat' (JNF matrices). The surrounding discussion is about matrices, so this is a typographical slip, but it could confuse readers unfamiliar with JNF.
  3. [Section 6, 'Positive operators and the Loewner order (definition)'] The construction of ≤ on non-square operators using heterogenous_cblinfun_id is surprising and is a technical device rather than a mathematically motivated definition. The paper does disclose this, but it would be helpful to add a sentence clarifying that for non-square types that are not unitarily isomorphic via the heterogeneous identity, the definition degenerates to equality, and that this is only a device to make the type-class instantiation work. The spelling 'heterogenous' (for the usual 'heterogeneous') is also worth a note, since it is used consistently in the constants.
  4. [Section 1.1, overview bullet list] The paper marks material with no real analogue using '▲' in the bullet list. This is a useful device, but it is not explained before the list. A one-line explanation of the symbol would make the overview easier to read.

Circularity Check

0 steps flagged

No significant circularity: machine-checked formalization with only external, prior AFP/distribution dependencies.

full rationale

This is a formalization paper, not an empirical derivation; its claims are machine-checked Isabelle/HOL lemmas built from explicit definitions. The construction of cblinfun, adjoints, projectors, the BLT extension theorem, the Loewner order, ell2, and the JNF correspondence is self-contained in the sense that definitions are given and theorems are proved from them. The only dependencies on material originally from the same authors are the Banach-Steinhaus theorem [37], cited as already formalized for real operators and lifted to the complex case by transfer, and the Infinite_Sum summability infrastructure, now included in HOL-Analysis. Both are machine-checked AFP/distribution entries whose assumptions do not include the target results, so under the review rules they count as external evidence rather than circular input. Definitional choices such as 'sandwich', the nonstandard 'rank1' predicate, and the heterogeneous Loewner-order construction are explicitly disclosed notation/design decisions, not predictions masquerading as derivations. No equation in the paper reduces to its own input, and no fitted parameter is relabeled as a result. Therefore no circularity is present.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 1 invented entities

The central claim rests on standard axioms of the proof assistant and of vector/inner-product spaces, plus imported library correctness. The only genuinely novel formalization device is the heterogeneous identity used for the Loewner order; it is documented and proves the intended properties, so it is an axiomatic construction rather than a hidden assumption. No free parameters are fitted to data.

axioms (6)
  • standard math HOL classical logic with excluded middle and axiom of choice is sound.
    The formalization is built in Isabelle/HOL; the paper states in Section 2 that HOL includes excluded middle and choice.
  • standard math Complex vector space axioms as given by the 'complex_vector' type class (additive group, compatible scalar multiplication, etc.).
    Stated in Section 3 as the axioms of the complex_vector class.
  • standard math Complex inner product space axioms as given by the 'complex_inner' type class.
    Stated in Section 4 as the axioms of the complex_inner class.
  • domain assumption one_dim class axioms: canonical_basis = [1], one_dim_prod_scale1, divide_inverse, one_dim_inverse.
    Introduced in Section 5 to ensure a canonical identification between one-dimensional spaces and C; these are imposed properties of the type class, not derived facts.
  • domain assumption Correctness of the imported Isabelle libraries: HOL-Analysis, Jordan_Normal_Form, and Infinite_Sum.
    The development relies on these libraries throughout (see Section 1.3 and referenced entries); if they were unsound, the new results would not be reliable.
  • domain assumption The heterogeneous identity construction (heterogenous_cblinfun_id) is definable and consistent in Isabelle/HOL.
    Used in Section 6 to define the Loewner order on operators between possibly different types; the paper describes the construction but the soundness is inherited from the logic itself.
invented entities (1)
  • heterogenous_cblinfun_id no independent evidence
    purpose: A function of type 'a ⇒CL 'b that is the identity when 'a = 'b and zero otherwise, used to define the Loewner order on arbitrary bounded operators.
    Introduced in Section 6 as a formalization device. It has no mathematical motivation beyond making the Loewner order type-ambiguous; it is not a new physical or mathematical entity and provides no falsifiable handle outside the formal framework.

pith-pipeline@v1.3.0-alltime-deepseek · 44044 in / 9726 out tokens · 96150 ms · 2026-08-03T18:15:58.273589+00:00 · methodology

0 comments
read the original abstract

We present a formalization of bounded operators on complex vector spaces in Isabelle/HOL. Our formalization contains material on complex vector spaces (normed spaces, Banach spaces, Hilbert spaces) that complements and goes beyond the developments of real vectors spaces in the Isabelle/HOL standard library. We define the type of bounded operators between complex vector spaces (cblinfun) and develop the theory of unitaries, projectors, extension of bounded linear functions (BLT theorem), adjoints, Loewner order, closed subspaces and more. For the finite-dimensional case, we provide code generation support by identifying finite-dimensional operators with matrices as formalized in the Jordan_Normal_Form AFP entry.

Figures

Figures reproduced from arXiv: 2512.05878 by Dominique Unruh, Jos\'e Manuel Rodr\'iguez Caballero.

Figure 1
Figure 1. Figure 1: Number of (non-blank) lines of code, definitions, and proven facts in our development. [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗

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

40 extracted references · 2 canonical work pages

  1. [1]

    Mathematical components library for the Rocq theorems prover [25]. 2025. [22]Mathlib.https://github.com/leanprover-community/mathlib4. Library of formalized mathe- matics for the Lean prover [18]. Version 4. Content overview in [1]. 2025

    2025

  2. [2]

    Quantum Security Proofs Using Semi- classical Oracles

    Andris Ambainis, Mike Hamburg, and Dominique Unruh. “Quantum Security Proofs Using Semi- classical Oracles”. In:Crypto 2019. Springer, 2019, pp. 269–295

    2019

  3. [3]

    Contributed with Isabelle distri- bution,https : / / isabelle

    Clemens Ballarin.Tutorial to Locales and Locale Interpretation. Contributed with Isabelle distri- bution,https : / / isabelle . in . tum . de / website - Isabelle2025 / dist / Isabelle2025 / doc / locales.pdf. 2025

    2025

  4. [4]

    The logic of quantum mechanics

    Garrett Birkhoff and John von Neumann. “The logic of quantum mechanics”. In:Annals of Math- ematics37.823 (1936).doi:10.2307/1968621

    doi:10.2307/1968621 1936

  5. [5]

    Con- tributed with Isabelle distribution,https : / / isabelle

    Jasmin Blanchette.Hammering Away – A User’s Guide to Sledgehammer for Isabelle/HOL. Con- tributed with Isabelle distribution,https : / / isabelle . in . tum . de / website - Isabelle2025 / dist/Isabelle2025/doc/sledgehammer.pdf. 2025

    2025

  6. [6]

    Contributed with Isabelle distribution,https://isabelle

    Jasmin Blanchette.Isabelle’s Logics. Contributed with Isabelle distribution,https://isabelle. in.tum.de/website-Isabelle2025/dist/Isabelle2025/doc/logics.pdf. The logic HOL that we use is described in Chapter 2. 2025

    2025

  7. [7]

    Complex Bounded Operators

    José Manuel Rodríguez Caballero and Dominique Unruh. “Complex Bounded Operators”. In: Archive of Formal Proofs(2021).https://isa-afp.org/entries/Complex_Bounded_Operators. html, Formal proof development.issn: 2150-914x

    2021

  8. [8]

    John B Conway.A course in functional analysis. Vol. 96. Springer Science & Business Media, 2013

    2013

  9. [9]

    Repository of formalizations in Isabelle [15], organized as a journal, ISSN: 2150-914x

    Manuel Eberl, Gerwin Klein, Peter Lammich, Andreas Lochbihler, Tobias Nipkow, Larry Paulson, René Thiemann, and Dmitriy Traytel, eds.Archive of Formal Proofs.https://www.isa-afp.org/, last accessed 2025-12-01. Repository of formalizations in Isabelle [15], organized as a journal, ISSN: 2150-914x. 2025. 216 ▷ top_ccsubspace_code 217 ▷ bot_as_span 218 ▷ spa...

    2025

  10. [10]

    Yuan Feng, Nengkun Yu, and Mingsheng Ying.Model checking quantum Markov chains. 2013. arXiv:1205.2187 [quant-ph].url:https://arxiv.org/abs/1205.2187

    Pith/arXiv arXiv 2013

  11. [11]

    Contributed with Isabelle distri- bution,https : / / isabelle

    Florian Haftmann.Code generation from Isabelle/HOL theories. Contributed with Isabelle distri- bution,https : / / isabelle . in . tum . de / website - Isabelle2025 / dist / Isabelle2025 / doc / codegen.pdf. 2025

    2025

  12. [12]

    Contributed with Isabelle distri- bution,https : / / isabelle

    Florian Haftmann.Haskell-style type classes with Isabelle/Isar. Contributed with Isabelle distri- bution,https : / / isabelle . in . tum . de / website - Isabelle2025 / dist / Isabelle2025 / doc / classes.pdf. 2025

    2025

  13. [13]

    Formalizing the One-Way to Hiding Theorem

    Katharina Heidler and Dominique Unruh. “Formalizing the One-Way to Hiding Theorem”. In:Pro- ceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CO, USA, January 20-21, 2025. Ed. by Kathrin Stark, Amin Timany, Sandrine Blazy, and Nicolas Tabareau. ACM, 2025, pp. 243–256.doi:10.1145/3703595.3705887

    arXiv 2025

  14. [14]

    Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL

    Brian Huffman and Ondřej Kunčar. “Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL”.In:Certified Programs and Proofs.SpringerInternationalPublishing,2013,pp.131– 146.doi:10.1007/978-3-319-03545-1_9. [15]Isabelle theorem prover. Distribution:https://isabelle.in.tum.de/. 2025

    work page doi:10.1007/978-3-319-03545-1_9 2013

  15. [16]

    Karl Kraus.States, effects, and operations: fundamental notions of quantum theory. Vol. 190. LNP. Springer, 1983.isbn: 0387127321

    1983

  16. [17]

    TheOnewaytoHidingTheorem

    KatharinaKreuzerandDominiqueUnruh.“TheOnewaytoHidingTheorem”.In:Archive of Formal Proofs(2025).https://isa-afp.org/entries/Oneway2Hiding.html, Formal proof development. Presented in [13].issn: 2150-914x. [18]Lean theorem prover.https://lean-lang.org/, last accessed 2025-12-02. 2025

    2025

  17. [19]

    Termination of nondeterministic quantum pro- grams

    Yangjia Li, Nengkun Yu, and Mingsheng Ying. “Termination of nondeterministic quantum pro- grams”. In:Acta Informatica51.1 (Oct. 2013), 1–24.issn: 1432-0525.doi:10.1007/s00236-013- 0185-3.url:http://dx.doi.org/10.1007/s00236-013-0185-3

    work page doi:10.1007/s00236-013- 2013

  18. [20]

    Formal Verification of Quantum Algorithms Using Quantum Hoare Logic

    Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. “Formal Verification of Quantum Algorithms Using Quantum Hoare Logic”. In: Computer Aided Verification. Cham: Springer, 2019, pp. 187–207.doi:10 . 1007 / 978 - 3 - 030 - 25543-5_12. [21]Mathematical Components,math-comp.https://math-comp.github.io/, ...

    2019

  19. [23]

    Contributed with Isabelle distribution, https : / / isabelle

    Tobias Nipkow.Programming and Proving in Isabelle/HOL. Contributed with Isabelle distribution, https : / / isabelle . in . tum . de / website - Isabelle2025 / dist / Isabelle2025 / doc / prog - prove.pdf. 2025

    2025

  20. [24]

    Federico Olmedo and Alejandro Díaz-Caro.Runtime Analysis of Quantum Programs: A Formal Approach. 2019. arXiv:1911.11247 [cs.LO]. [25]Rocq theorem prover.https://rocq-prover.org/, last accessed 2025-12-02. Formally called Coq. 2025

    Pith/arXiv arXiv 2019

  21. [26]

    Quantum Programming

    J. W. Sanders and P. Zuliani. “Quantum Programming”. In:Mathematics of Program Construction. Ed. by Roland Backhouse and José Nuno Oliveira. Berlin, Heidelberg: Springer Berlin Heidelberg, 2000, pp. 80–99.isbn: 978-3-540-45025-2. [27]SessionHOL-Analysis.https://isabelle.in.tum.de/website-Isabelle2025/dist/library/ HOL/HOL-Analysis/index.html. Collection o...

    2000

  22. [29]

    Formalizing Jordan normal forms in Isabelle/HOL

    René Thiemann and Akihisa Yamada. “Formalizing Jordan normal forms in Isabelle/HOL”. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. CPP 2016. St. Petersburg, FL, USA: Associationfor Computing Machinery, 2016, 88–99.isbn: 9781450341271. doi:10.1145/2854065.2854073

    arXiv 2016

  23. [30]

    Matrices, Jordan Normal Forms, and Spectral Radius Theory

    René Thiemann and Akihisa Yamada. “Matrices, Jordan Normal Forms, and Spectral Radius Theory”. In:Archive of Formal Proofs(2015).https://isa-afp.org/entries/Jordan_Normal_ Form.html, Formal proof development. Presented in [29].issn: 2150-914x

    2015

  24. [31]

    Dominique Unruh.dominique-unruh/qrhl-tool: Proof assistant for qRHL. GitHub. Based on the logic from [35]. 2017-2025.url:https://dominique-unruh.github.io/qrhl-tool/

    2017

  25. [32]

    Kraus Maps

    Dominique Unruh. “Kraus Maps”. In:Archive of Formal Proofs(2025).https://isa-afp.org/ entries/Kraus_Maps.html, Formal proof development.issn: 2150-914x

    2025

  26. [33]

    Quantum and Classical Registers

    Dominique Unruh. “Quantum and Classical Registers”. In:Archive of Formal Proofs(2021).https: //isa-afp.org/entries/Registers.html, Formal proof development.issn: 2150-914x

    2021

  27. [34]

    arXiv:2105.10914v3 [cs.LO]

    Dominique Unruh.Quantum references. arXiv:2105.10914v3 [cs.LO]. 2024

    Pith/arXiv arXiv 2024

  28. [35]

    Quantum relational Hoare logic

    Dominique Unruh. “Quantum relational Hoare logic”. In:Proc. ACM Program. Lang.3 (Jan. 2019). Proceedings of POPL 2019. Full version is arXiv:1802.03188 [quant-ph], 33:1–33:31.issn: 2475- 1421.doi:10.1145/3290346.url:http://doi.acm.org/10.1145/3290346

    Pith/arXiv arXiv 2019

  29. [36]

    The Tensor Product on Hilbert Spaces

    Dominique Unruh. “The Tensor Product on Hilbert Spaces”. In:Archive of Formal Proofs(2024). https://isa-afp.org/entries/Hilbert_Space_Tensor_Product.html, Formal proof develop- ment.issn: 2150-914x

    2024

  30. [37]

    Banach-Steinhaus Theorem

    Dominique Unruh and José Manuel Rodríguez Caballero. “Banach-Steinhaus Theorem”. In:Archive of Formal Proofs(2020).https://isa-afp.org/entries/Banach_Steinhaus.html, Formal proof development.issn: 2150-914x

    2020

  31. [38]

    Contributed with Isabelle distribution,https://isabelle.in

    Makarius Wenzel.Isabelle/jEdit. Contributed with Isabelle distribution,https://isabelle.in. tum.de/website-Isabelle2025/dist/Isabelle2025/doc/jedit.pdf. 2025

    2025

  32. [39]

    Contributed with Isabelle distribution, https : / / isabelle

    Makarius Wenzel.The Isabelle/Isar Reference Manual. Contributed with Isabelle distribution, https : / / isabelle . in . tum . de / website - Isabelle2025 / dist / Isabelle2025 / doc / isar - ref.pdf. 2025

    2025

  33. [40]

    Mathematics Stack Exchange,https://math

    Eric Wofsey.Sum of closed spaces is not closed. Mathematics Stack Exchange,https://math. stackexchange.com/q/1786792(version: 2016-05-15)

    arXiv 2016

  34. [41]

    Floyd–Hoare Logic for Quantum Programs

    Mingsheng Ying. “Floyd–Hoare Logic for Quantum Programs”. In:ACM Trans. Program. Lang. Syst.33.6 (2012), 19:1–19:49.issn: 0164-0925.doi:10.1145/2049706.2049708

    arXiv 2012

  35. [42]

    Predicate transformer semantics of quantum programs

    Mingsheng Ying, Runyao Duan, Yuan Feng, and Zhengfeng Ji. “Predicate transformer semantics of quantum programs”. In:Semantic Techniques in Quantum Computation. Ed. by Simon Gay and Ian Mackie. Cambridge University Press, 2009. Chap. 8, 311–360.doi:10.1017/CBO9781139193313. 009

    doi:10.1017/cbo9781139193313 2009

  36. [43]

    Invariants of quantum programs: characteri- sations and generation

    Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. “Invariants of quantum programs: characteri- sations and generation”. In:Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. ACM, Jan. 2017.doi:10.1145/3009837.3009840

    arXiv 2017

  37. [44]

    Earlier version of [45] with partially different results

    Nengkun Yu.Quantum Temporal Logic. Earlier version of [45] with partially different results. 2019. arXiv:1908.00158 [cs.LO].url:https://arxiv.org/abs/1908.00158

    Pith/arXiv arXiv 2019

  38. [45]

    Quantum temporal logic and reachability problems of matrix semigroups

    Nengkun Yu. “Quantum temporal logic and reachability problems of matrix semigroups”. In:Inf. Comput.300.C (Oct. 2024). A revision of [44] with partially different results.issn: 0890-5401.doi: 10.1016/j.ic.2024.105197

    arXiv 2024

  39. [46]

    A Quantum Interpretation of Bunched Logic & Quantum Separation Logic

    Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, and Nengkun Yu. “A Quantum Interpretation of Bunched Logic & Quantum Separation Logic”. In:2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Full version is arXiv:2102.00329v1 [cs.LO]. 2021, pp. 1–14. doi:10.1109/LICS52264.2021.9470673

    Pith/arXiv arXiv 2021

  40. [47]

    An applied quantum Hoare logic

    Li Zhou, Nengkun Yu, and Mingsheng Ying. “An applied quantum Hoare logic”. In:PLDI 2021. ACM, June 2019.doi:10.1145/3314221.3314584. 35 Symbol index ▷ lemma_nameReference to the name of a lemma in the Isabelle theories |b⟩Basis vector in Hilbert space’a ell2 ⟨b|Adjoint of⟨b| CComplex numbers NNatural numbers |x|Absolute value ofx ∥x∥Norm of vectorx,norm A...

    arXiv 2021