Deriving Program Logics from 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 follow from the axioms of imperative categories. The algebra of guarded commands derived by the categorical structure generalises guarded Kleene algebras with tests.

arXiv comment59 pages, including appendix