Deriving Program Logics from Distributive Monoidal Categories
Filippo Bonchi, Elena Di Lavore, Mario Román, Sam Staton · arXiv (Cornell University) · 2025
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.