{"id":"arxiv/2607.17714","url":"https://arxiv.org/abs/2607.17714","tags":["quant-ph","cs.LO"],"score":0,"title":"Formal Verification of Continuous-Variable Quantum Programs","domain":"quant-ph","source":"arxiv","authors":["Stefanie Muroya","Thomas A. Henzinger"],"reviews":0,"subject":"quant-ph","summary":"We provide a formal framework for Continuous-Variable Quantum Computing (CQC). While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for continuous-variable quantum programs nor of a unary Hoare logic for their verification. There are several technical obstacles to extending to CQC any of the formal frameworks available for Discrete-Variable Quantum Computing (DQC). Most importantly, continuous-variable quantum programs act on {\\em infinite-dimensional} Hilbert spaces; their measurement outcomes are often {\\em unbounded} and have expected values that are…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-07-20","reactions":{}}