In this paper, we define an assertion language designed for expectation-based reasoning about quantum programs. The key design idea is a representation of quantum predicates by quasi-probability distributions of generalized Pauli operators. Then we extend classical techniques such as Gödelization to prove that this language is expressive with respect to the quantum programs with loops—specifically, for any program $S$ and any postcondition $\psi$ formulated in the assertion language, the weakest precondition of $S$ with respect to $\psi$ can also be expressed as a formula in the assertion language. As an application, we present a sound and relatively complete quantum Hoare logic upon our expressive assertion language.
Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:40 | Quantum 1POPL at Dortoirs Chair(s): Ugo Dal Lago University of Bologna; Centre Inria d’Université Côte d’Azur | ||
14:00 25mTalk | An Expressive Assertion Language for Quantum Programs POPL Bonan Su Tsinghua University, Yuan Feng Tsinghua University, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University, Li Zhou Institute of Software at Chinese Academy of Sciences DOI | ||
14:25 25mTalk | Hadamard-Pi: Equational Quantum Programming POPL Wang Fang University of Edinburgh, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark DOI | ||
14:50 25mTalk | Qudit Quantum Programming with Projective Cliffords POPL DOI | ||
15:15 25mTalk | RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing POPL Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University, Emanuele D'Osualdo University of Konstanz DOI Pre-print | ||