A comprehensive, machine-checked Isabelle/HOL formalization of complex Hilbert spaces and bounded operators, including adjoints, unitaries, projectors, the BLT extension theorem, Loewner order, and ℓ2 spaces.
Termination of nondeterministic quantum pro- grams
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
fields
cs.LO 1years
2025 1verdicts
ACCEPT 1representative citing papers
citing papers explorer
-
Complex Bounded Operators in Isabelle/HOL
A comprehensive, machine-checked Isabelle/HOL formalization of complex Hilbert spaces and bounded operators, including adjoints, unitaries, projectors, the BLT extension theorem, Loewner order, and ℓ2 spaces.