Email Gateway (Aug 22 2022 at 19:23): Email Gateway (Aug 22 2022 at 19:23):From: Tobias Nipkow <nipkow@in.tum.de>
Quantum Hoare Logic
Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li,
Mingsheng Ying and Naijun Zhan
We formalize quantum Hoare logic as given in [1]. In particular, we specify the
syntax and denotational semantics of a simple model of quantum programs. Then,
we write down the rules of quantum Hoare logic for partial correctness, and show
the soundness and completeness of the resulting proof system. As an application,
we verify the correctness of Grover’s algorithm.
https://www.isa-afp.org/entries/QHLProver.html
smime.p7s
Last updated: Apr 30 2024 at 08:19 UTC