D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation
Abstract
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 supported by a rich equational theory for proving equality between expressions in the language. These proofs are typically carried on pen-and-paper, and can be exceedingly long and error-prone. We introduce D-Hammer, the first tool to support automated equational proof for labelled Dirac notation. The salient features of D-Hammer include: an expressive, higher-order, dependently-typed language for labelled Dirac notation; an efficient normalization algorithm; and an optimized C++ implementation. We evaluate the implementation on representative examples from both plain and labelled Dirac notation. In the case of plain Dirac notation, we show that our implementation significantly outperforms DiracDec.
Keywords
Cite
@article{arxiv.2505.08633,
title = {D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation},
author = {Yingte Xu and Li Zhou and Gilles Barthe},
journal= {arXiv preprint arXiv:2505.08633},
year = {2025}
}
Comments
This version of the contribution has been accepted for publication, after peer review but is not the Version of Record and does not reflect post-acceptance improvements, or any corrections. 47 pages (with appendix)