Reasoning about Continuous-Variable Quantum Systems
The work developed a formal semantics and proof system for Continuous-Variable Quantum Computing (CVQC) to verify program correctness. It introduced closed positive quadratic forms as predicates to handle unbounded continuous values, allowing for reasoning about finite expectations and infinite penalties. This system successfully bridges continuous quantum dynamics with rigorous Hoare logic, enabling the verification of complex CV quantum algorithms by providing precise quantitative bounds on physical properties like variance.