Program Logics via Distributive Monoidal Categories
Logic in Computer Science
2025-07-25 v1
Abstract
We derive multiple program logics, including correctness, incorrectness, and relational Hoare logic, from the axioms of imperative categories: uniformly traced distributive copy-discard categories. We introduce an internal language for imperative multicategories, on top of which we derive combinators for an adaptation of Dijkstra's guarded command language. Rules of program logics are derived from this internal language.
Keywords
Cite
@article{arxiv.2507.18238,
title = {Program Logics via Distributive Monoidal Categories},
author = {Filippo Bonchi and Elena Di Lavore and Mario Román and Sam Staton},
journal= {arXiv preprint arXiv:2507.18238},
year = {2025}
}
Comments
52 pages, including appendix