Local Variables and Quantum Relational Hoare Logic

TL;DR

This paper extends quantum relational Hoare logic by incorporating local variables, providing new reasoning rules and enhancing a verification tool for better quantum program analysis.

Contribution

Introduction of local variables into qRHL, new reasoning rules including an improved adversary rule, and extension of the qrhl-tool for verification.

Findings

Enhanced reasoning capabilities for quantum programs with local variables

Extended verification tool supports new rules and local variable analysis

Improved adversary rule strengthens security proofs in quantum settings

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.