2019/03/31 by Yangjia Li, Dominique Unruh
Computer Science · Physics and Astronomy · #cs.LO #quant-ph
paper · pdf · doi:10.4230/lipics.icalp.2021.136
published as ICALP 2021, track B
arxiv created 2021/07/12 · arxiv updated 2021/07/13
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.