Quantum Relational Hoare Logic with Expectations

Authors Yangjia Li, Dominique Unruh

Thumbnail PDF


  • Filesize: 0.93 MB
  • 20 pages

Document Identifiers

Author Details

Yangjia Li
  • University of Tartu, Estonia
  • SKLCS, Institute of Software, CAS, Beijing, China
Dominique Unruh
  • University of Tartu, Estonia


We thank Gilles Barthe, Tore Vincent Carstens, and Justin Hsu for valuable discussions.

Cite AsGet BibTex

Yangjia Li and Dominique Unruh. Quantum Relational Hoare Logic with Expectations. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 136:1-136:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


We present a variant of the quantum relational Hoare logic from (Unruh, POPL 2019) that allows us to use "expectations" in pre- and postconditions. That is, when reasoning about pairs of programs, our logic allows us to quantitatively reason about how much certain pre-/postconditions are satisfied that refer to the relationship between the programs inputs/outputs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Quantum computation theory
  • Theory of computation → Hoare logic
  • Theory of computation → Program verification
  • Quantum cryptography
  • Hoare logics
  • formal verification


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub. Easycrypt: A tutorial. In FOSAD 2012/2013 Tutorial Lectures, pages 146-166. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10082-1_6.
  2. Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In Crypto 2011, volume 6841 of LNCS, pages 71-90. Springer, 2011. Google Scholar
  3. Gilles Barthe, Benjamin Grégoire, Federico Olmedo, and Santiago Zanella Béguelin. CertiCrypt: Computer-aided cryptographic proofs in Coq. http://certicrypt.gforge.inria.fr/. Accessed 2018-10-24.
  4. Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Formal certification of code-based cryptographic proofs. In POPL 2009, pages 90-101. ACM, 2009. URL: https://doi.org/10.1145/1480881.1480894.
  5. Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. Relational proofs for quantum programs. Proc. ACM Program. Lang., 4:21:1-21:29, 2019. Proceedings of POPL 2020. Full version is http://arxiv.org/abs/1901.05184v2. URL: https://doi.org/10.1145/3371089.
  6. Nick Benton. Simple relational correctness proofs for static analyses and program transformations. In POPL '04, pages 14-25. ACM, 2004. URL: https://doi.org/10.1145/964001.964003.
  7. Rohit Chadha, Paulo Mateus, and Amílcar Sernadas. Reasoning about imperative quantum programs. ENTCS, 158:19-39, 2006. URL: https://doi.org/10.1016/j.entcs.2006.04.003.
  8. John B. Conway. A course in functional analysis. Number 96 in Graduate texts in mathematics. Springer, 2nd ed edition, 1997. Google Scholar
  9. John B. Conway. A course in operator theory. Number 21 in Graduate studies in mathematics. American Mathematical Society, Providence, RI, 2000. Google Scholar
  10. Ellie D'Hondt and Prakash Panangaden. Quantum weakest preconditions. Mathematical. Structures in Comp. Sci., 16(3):429-451, 2006. URL: https://doi.org/10.1017/S0960129506005251.
  11. Yuan Feng, Runyao Duan, Zhengfeng Ji, and Mingsheng Ying. Proof rules for the correctness of quantum programs. Theoretical Computer Science, 386(1):151-166, 2007. URL: https://doi.org/10.1016/j.tcs.2007.06.011.
  12. Yoshihiko Kakutani. A logic for formal verification of quantum programs. In Anupam Datta, editor, ASIAN 2009, pages 79-93, Berlin, Heidelberg, 2009. Springer. Google Scholar
  13. Dexter Kozen. A probabilistic PDL. In STOC '83, pages 291-297, New York, NY, USA, 1983. ACM. URL: https://doi.org/10.1145/800061.808758.
  14. Yangjia Li and Mingsheng Ying. Algorithmic analysis of termination problems for quantum programs. Proc. ACM Program. Lang., 2:35:1-35:29, 2018. Proceedings of POPL 2019. URL: https://doi.org/10.1145/3158123.
  15. Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, Cambridge, 10th anniversary edition, 2010. Google Scholar
  16. Dominique Unruh. dominique-unruh/qrhl-tool: Prototype proof assistant for qRHL. GitHub, 2018. URL: https://github.com/dominique-unruh/qrhl-tool.
  17. Dominique Unruh. Quantum relational Hoare logic. Proc. ACM Program. Lang., 3:33:1-33:31, January 2019. Proceedings of POPL 2019. Full version is https://arxiv.org/abs/1802.03188 [quant-ph]. URL: https://doi.org/10.1145/3290346.
  18. Mingsheng Ying. Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst., 33(6):19:1-19:49, 2012. URL: https://doi.org/10.1145/2049706.2049708.