A Diagrammatic Algebra for Program Logics

Filippo Bonchi, Alessandro Di Giorgio, Elena Di Lavore

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…