3 papers
quant-ph2026
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…
cs.PL2025
D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation
Yingte Xu, Li Zhou, Gilles Barthe
Labelled Dirac notation is a formalism commonly used by physicists to represent many-body quantum systems and by computer scientists to assert properties of quantum programs. It is…
cs.PL2024
Automating Equational Proofs in Dirac Notation
Yingte Xu, Gilles Barthe, Li Zhou
Dirac notation is widely used in quantum physics and quantum programming languages to define, compute and reason about quantum states. This paper considers Dirac notation from the…