4 citations · 4 across the 3 of their papers we have counts for
4 papers
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…
Complete Quantum Relational Hoare Logics from Optimal Transport Duality
Gilles Barthe, Minbo Gao, Theo Wang +1
We introduce a quantitative relational Hoare logic for quantum programs. Assertions of the logic range over a new infinitary extension of positive semidefinite operators. We prove…
Laws of Quantum Programming
Mingsheng Ying, Li Zhou, Gilles Barthe
In this paper, we investigate the fundamental laws of quantum programming. We extend a comprehensive set of Hoare et al.'s basic laws of classical programming to the quantum settin…
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…