A Diagrammatic Basis for Computer Programming

TL;DR

This work introduces Kleene-Cartesian rig categories, namely rig categories where $\otimes$ provides a Cartesian bicategory, while $\oplus$ a Kleene bicategory, and shows that the associated tape diagrams can conveniently deal with imperative programs and various program logic.

Abstract

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.