Relational program verification is a variant of program verification
where one can reason about two programs and as a special case about
two executions of a single program on different inputs. Relational
program verification can be used for reasoning about a broad range of
properties, including equivalence and refinement, and specialized
notions such as continuity, information flow security or relative
cost. In a higher-order setting, relational program verification can
be achieved using relational refinement type systems, a form of
refinement types where assertions have a relational interpretation.
Relational refinement type systems excel at relating structurally
equivalent terms but provide limited support for relating terms with
very different structures.

We present a logic, called Relational Higher Order Logic (RHOL), for
proving relational properties of a simply typed $\lambda$-calculus
with inductive types and recursive definitions. RHOL retains the
type-directed flavour of relational refinement type systems but
achieves greater expressivity through rules which simultaneously
reason about the two terms as well as rules which only contemplate one
of the two terms. We show that RHOL has strong foundations, by proving
an equivalence with higher-order logic (HOL), and leverage this
equivalence to derive key meta-theoretical properties: subject
reduction, admissibility of a transitivity rule and set-theoretical
soundness. Moreover, we define sound embeddings for several existing
relational type systems such as relational refinement types and type
systems for dependency analysis and relative cost, and we verify
examples that were out of reach of prior work.