Build a Learning Habit
Download Class Central's free printable study calendar
Download for Free
This video presents a research talk from POPL 2025 that explores automated reasoning techniques for Dirac notation, a mathematical formalism widely used in quantum physics and quantum programming languages. Learn how researchers Yingte Xu, Gilles Barthe, and Li Zhou prove the decidability of the first-order theory of Dirac notation through reduction to the theory of real closed fields, and demonstrate an efficient algorithm for checking equation validity using term-rewriting techniques. The presentation showcases their implementation in Mathematica and its application across over 100 examples from the literature. The research has been recognized with "Artifacts Available" and "Artifacts Evaluated — Reusable" badges, with supplementary materials available through Zenodo. The complete paper can be accessed through the ACM Digital Library.
