@inproceedings{b51a47b60a55467a8f04bb9b8e4a2f5d,
title = "An applied quantum hoare logic",
abstract = "We derive a variant of quantum Hoare logic (QHL), called applied quantum Hoare logic (aQHL for short), by: (1) restricting QHL to a special class of preconditions and postconditions, namely projections, which can significantly simplify verification of quantum programs and are much more convenient when used in debugging and testing; and (2) adding several rules for reasoning about robustness of quantum programs, i.e. error bounds of outputs. The effectiveness of aQHL is shown by its applications to verify two sophisticated quantum algorithms: HHL (Harrow-Hassidim-Lloyd) for solving systems of linear equations and qPCA (quantum Principal Component Analysis).",
keywords = "Hoare logic, Programming languages, Projections, Quantum computation, Robustness",
author = "Li Zhou and Nengkun Yu and Mingsheng Ying",
note = "Publisher Copyright: {\textcopyright} 2019 Association for Computing Machinery.; 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019 ; Conference date: 22-06-2019 Through 26-06-2019",
year = "2019",
month = jun,
day = "8",
doi = "10.1145/3314221.3314584",
language = "English",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
publisher = "Association for Computing Machinery",
pages = "1149--1162",
editor = "McKinley, \{Kathryn S.\} and Kathleen Fisher",
booktitle = "PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation",
}