We introduce Kleene bicategories. In the same way that cartesian bicategories of relations capture the structure of relations with cartesian product, Kleene bicategories capture the structure of relations with disjoint union. Kleene-cartesian bicategories combine these two structures by distributing the cartesian product over the disjoint union, and are expressive enough to deal with imperative programs. The derivation rules of Hoare logic follow from the axioms of Kleene-cartesian bicategories.

This talk is based on recent joint work with Filippo Bonchi and Alessandro Di Giorgio.