A Diagrammatic Algebra for Program Logics

Tape diagrams provide a convenient graphical notation for arrows of rig categories, i.e., categories equipped with two monoidal products, $$\oplus $$ ⊕ and $$\otimes $$ ⊗ . In this work, we introduce Kleene-Cartesian rig categories, namely rig categories where $$\otimes $$ ⊗ provides a Cartesian bicategory, while $$\oplus $$ ⊕ a Kleene bicategory.We show that the associated tape diagrams can conveniently deal with Hoare logic.