Showing cs.PLShow all
3 papers · 1 filter
cs.PL2025
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…
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…