Local Variables and Quantum Relational Hoare Logic
Logic in Computer Science
2020-07-29 v1
Abstract
We add local variables to quantum relational Hoare logic (Unruh, POPL 2019). We derive reasoning rules for supporting local variables (including an improved "adversary rule"). We extended the qrhl-tool for computer-aided verification of qRHL to support local variables and our new reasoning rules.
Cite
@article{arxiv.2007.14155,
title = {Local Variables and Quantum Relational Hoare Logic},
author = {Dominique Unruh},
journal= {arXiv preprint arXiv:2007.14155},
year = {2020}
}