A Diagrammatic Basis for Computer Programming
For computer scientists and logicians, it provides a unified graphical framework for reasoning about imperative programs, but the work is incremental as it extends existing categorical structures.
The paper introduces Kleene-Cartesian rig categories, combining Cartesian and Kleene bicategories, and shows that their tape diagrams can model imperative programs and program logic.
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 imperative programs and various program logic.