Program Logics via Distributive Monoidal Categories

We derive multiple program logics, including correctness, incorrectness, and relational Hoare logic, from the axioms of imperative categories: uniformly traced distributive copy-discard categories. We introduce an internal language for imperative multicategories, on top of which we derive combinators for an adaptation of Dijkstra’s guarded command language. Rules of program logics are derived from this internal language.