2024/10/04 by Filippo Bonchi, Bonchi, Filippo, Alessandro Di Giorgio +3 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2410.03561
openalex publication_date 2024/10/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Tape diagrams provide a convenient notation for arrows of rig categories, i.e., categories equipped with two monoidal products, ⊕ and ⊗, where ⊗ distributes over ⊕ . In this work, we extend tape diagrams with traces over ⊕ 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 ⊗ is a cartesian bicategory, while the one provided by ⊕ 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.