Content area
Tape diagrams provide a convenient notation for arrows of rig categories, i.e., categories equipped with two monoidal products, \(\oplus\) and \(\otimes\), where \(\otimes\) distributes over \(\oplus \). In this work, we extend tape diagrams with traces over \(\oplus\) in order to deal with iteration in imperative programming languages. More precisely, we introduce Kleene-Cartesian bicategories, namely rig categories where the monoidal structure provided by \(\otimes\) is a cartesian bicategory, while the one provided by \(\oplus\) is what we name a Kleene bicategory. We show that the associated language of tape diagrams is expressive enough to deal with imperative programs and the corresponding laws provide a proof system that is at least as powerful as the one of Hoare logic.