4 papers · 1 filter
Quantum Uncomputation of Clean and Dirty Ancilla Qubits
Chenke Liu, Li Zhou, Boning Meng
Automatic uncomputation aims to provide programming-language-level support to facilitate the correct and safe use of ancilla qubits in quantum computing, but efforts have only been…
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…
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…
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…