# Thirty-seven years of relational Hoare logic: remarks on its principles and history

arXiv: https://arxiv.org/abs/2007.06421 · HTML: https://mlsanity.com/paper/2007.06421/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Jul 2020.

## Built on by (most cited first, 1 of 1)

- [Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI](https://mlsanity.com/paper/2608.00882/) (2026)

## Abstract (arXiv)

Relational Hoare logics extend the applicability of modular, deductive verification to encompass important 2-run properties including dependency requirements such as confidentiality and program relations such as equivalence or similarity between program versions. A considerable number of recent works introduce different relational Hoare logics without yet converging on a core set of proof rules. This paper looks backwards to little known early work. This brings to light some principles that clarify and organize the rules as well as suggesting a new rule and a new notion of completeness.