Deriving Program Logics from Distributive Monoidal Categories

Abstract: We propose imperative categories—uniformly traced distributive copy-discard categories—as a categorical semantics for imperative programs with commutative effects. Rules of multiple program logics, including correctness, incorrectness, and relational Hoare logic, follow from the axioms of imperative categories. The algebra of guarded commands derived by the categorical structure generalises guarded Kleene algebras with tests. This is recent joint work with Filippo Bonchi, Mario Román and Sam Staton.

logic in computer sciencecategory theorylogic

Audience: researchers in the topic

Online logic seminar

Series comments: Description: Seminar on all areas of logic