Document Open Access Logo

Quantum Relational Hoare Logic with Expectations

Authors Yangjia Li, Dominique Unruh

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.136.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

Funding

By the Air Force Office of Scientific Research through the project "Verification of quantum cryptography" (AOARD Grant FA2386-17-1-4022). By the project "Research and preparation of an ERC grant application on Certified Quantum Security" (MOBERC12). By the ERC consolidator grant CerQuS (819317). By the PRG team grant "Secure Quantum Technology" (PRG946) from the Estonian Research Council.
  • Li, Yangjia: By the National Natural Science Foundation of China (Grant No: 61872342).
  • Unruh, Dominique: By institutional research funding IUT2-1 of the Estonian Ministry of Education and Research. By the Estonian Centre of Exellence in IT (EXCITE) funded by the ERDF.

Acknowledgements

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)
https://doi.org/10.4230/LIPIcs.ICALP.2021.136

Abstract

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
Keywords
  • Quantum cryptography
  • Hoare logics
  • formal verification

Metrics

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

Related Versions

References

  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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact