Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions
This work provides foundational logical tools for reasoning about infinite-dimensional quantum programs, addressing a key gap in quantum program verification.
The paper presents sound and complete relational program logics for infinite-dimensional quantum and classical-quantum programs, using self-adjoint unbounded linear relations as assertions. It establishes completeness via new convergence and duality theorems for infinite-dimensional quantum states.
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.