Reasoning about Continuous-Variable Quantum Systems
Abstract
Continuous-variable quantum computing (CVQC) is a computing paradigm in which measurements yield values over a continuous domain. CVQC is both a convenient computational framework for modeling physical quantum systems, and a good abstraction for hardware platforms based on quantum optics. Yet, the semantic foundations of CVQC remain underdeveloped. To address this gap, we develop a formal semantics for a core CV quantum programming language, and sound verification methods for program correctness. A main contribution of this work is to isolate a well-behaved quantitative predicate domain that achieves sufficient expressiveness to accommodate unbounded values as they arise in the infinite-dimensional, continuous setting. Specifically, we choose closed positive quadratic forms as semantic predicates, representing finite expectations, domains of finiteness, and infinite penalties in one ordered object. We validate our choice by establishing that our semantic predicates satisfy desirable closure properties including the definition of weakest preconditions. We validate our design with two case studies, including an example based on the celebrated GKP error-correcting code, for which we establish a second moment bound.
Related
- Optimal Nonparametric Estimation of Phase-Space Representations for Non-Gaussian Continuous Variable Quantum States
- Efficient Quantum Simulation of Variable-Coefficient Transport with Continuous Source Injection
- Classical methods for modern applications: synthetic tabular data generation using lightweight discrete response continuous latent variable model
- Composite Variable Strategies for Continuous Endpoints
- Towards Intelligent Investment Risk Modeling: Probabilistic Reasoning and Adaptive Decision Systems Under Uncertainty
BibTeX
@misc{yu2026reasoning,
title = {{Reasoning about Continuous-Variable Quantum Systems}},
author = {Tianshi Yu and Gilles Barthe and Minbo Gao and Mingsheng Ying and Li Zhou},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2607.23137},
eprint = {2607.23137},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2607.23137},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Reasoning about Continuous-Variable Quantum Systems
AU - Tianshi Yu
AU - Gilles Barthe
AU - Minbo Gao
AU - Mingsheng Ying
AU - Li Zhou
PY - 2026
DA - 2026/10/19
PB - arXiv
DO - 10.48550/arxiv.2607.23137
UR - https://arxiv.org/abs/2607.23137
AB - Continuous-variable quantum computing (CVQC) is a computing paradigm in which measurements yield values over a continuous domain. CVQC is both a convenient computational framework for modeling physical quantum systems, and a good abstraction for hardware platforms based on quantum optics. Yet, the semantic foundations of CVQC remain underdeveloped. To address this gap, we develop a formal semantics for a core CV quantum programming language, and sound verification methods for program correctness. A main contribution of this work is to isolate a well-behaved quantitative predicate domain that achieves sufficient expressiveness to accommodate unbounded values as they arise in the infinite-dimensional, continuous setting. Specifically, we choose closed positive quadratic forms as semantic predicates, representing finite expectations, domains of finiteness, and infinite penalties in one ordered object. We validate our choice by establishing that our semantic predicates satisfy desirable closure properties including the definition of weakest preconditions. We validate our design with two case studies, including an example based on the celebrated GKP error-correcting code, for which we establish a second moment bound.
ER -