Email Gateway (Aug 22 2022 at 18:56): Email Gateway (Aug 22 2022 at 18:56):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
In the paper
@article{liu2016theorem,
title={A theorem prover for quantum Hoare logic and its applications},
author={Liu, Tao and Li, Yangjia and Wang, Shuling and Ying, Mingsheng
and Zhan, Naijun},
journal={arXiv preprint arXiv:1601.03835},
year={2016}
}
Link to the paper: https://arxiv.org/pdf/1601.03835.pdf
Link to the repository: https://github.com/ijcar2016/propitious-barnacle
the authors wrote:
By applying the theorem prover, verifying a quantum program against a
Isabelle/HOL has changed a lot since the time when that paper was wrote
(2016). Is there an elegant and practical way today in order to perform
such computations within Isabelle/HOL, i.e., without appealing to an
oracle? Is there some link to an existing solution?
Kind Regards,
José M.
Last updated: Apr 24 2024 at 01:07 UTC