Program logics via distributive monoidal categories

Abstract

We derive multiple program logics, including correctness, incorrectness, and relational Hoare logic, from the axioms of imperative categories: uniformly traced distributive copy-discard categories. Rules of program logics are derived from this categorical structure.