Quantum Relational Hoare Logic with Expectations
Logic in Computer Science
2021-07-13 v2 Quantum Physics
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.
Cite
@article{arxiv.1903.08357,
title = {Quantum Relational Hoare Logic with Expectations},
author = {Yangjia Li and Dominique Unruh},
journal= {arXiv preprint arXiv:1903.08357},
year = {2021}
}