Completeness of Relational Hoare Logics for Universal and Existential Properties

This paper proves alignment completeness of relational Hoare logics for both universal (∀∀) and existential (∀∃) relational properties. It also introduces sound rules that enable reasoning about relational properties beyond the scope of prior relational Hoare logics.