Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions
arXiv:2510.07051
Abstract
We present sound and complete relational program logics for infinite-dimensional quantum and classical-quantum programs. The logics model assertions as self-adjoint unbounded linear relations, which simultaneously support quantitative and qualitative reasoning. Our main theoretical results include new convergence theorems and infinite-dimensional duality theorems for infinite-dimensional quantum states, which we use to establish completeness.
65 pages, 8 figures, 3 tables. Full version of the paper accepted to LICS 2026