Quantum Relational Hoare Logic with Expectations

TL;DR

This paper introduces a quantum relational Hoare logic that incorporates expectations, enabling quantitative reasoning about program pairs' input-output relationships in quantum computing.

Contribution

It extends previous quantum relational Hoare logic by integrating expectations into pre- and postconditions for more nuanced program analysis.

Findings

Allows quantitative reasoning about program relationships

Enables analysis of how well conditions are satisfied

Builds on and extends prior quantum logic frameworks

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.