A Diagrammatic Algebra for Program Logics

TL;DR

This paper introduces a diagrammatic algebra using tape diagrams extended with traces to model iteration in imperative programming, providing a proof system comparable to Hoare logic.

Contribution

It develops Kleene-Cartesian bicategories combining rig categories with trace structures, enabling diagrammatic reasoning about imperative programs.

Findings

Tape diagrams extended with traces effectively model program iteration.

The resulting proof system matches the power of Hoare logic.

The algebraic framework offers a visual and formal approach to program verification.

Abstract

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.