Algorithmic Analysis of Termination Problems for Quantum Programs

Watch a 25-minute conference presentation from POPL 2018 exploring the algorithmic analysis of quantum program termination through linear ranking super-martingales (LRSM). Learn how researchers from the Chinese Academy of Sciences, University of Technology Sydney, and Tsinghua University developed termination theorems that reduce quantum program termination problems to the realisability and synthesis of LRSMs using Semi-Definite Programming. Discover novel applications of Gleason's theorem from quantum mechanics and a generalized Farkas' lemma for analyzing termination in quantum programs, including practical examples like quantum random walks and quantum Bernoulli factory for random number generation. Gain insights into how constraint-based approaches from probabilistic programming can be extended to the quantum domain through this technical presentation that bridges quantum physics, programming languages, and algorithmic analysis.