# 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.

## Key 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.

---
Source: https://tomesphere.com/paper/1903.08357