Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions

Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan +7

We present sound and complete relational program logics for infinite-dimensional quantum and classical-quantum programs. The logics model assertions as self-adjoint unbounded linea…