Program Logics via Distributive Monoidal Categories
Filippo Bonchi, Elena Di Lavore, Mario Rom\'an, Sam Staton
TL;DR
This paper develops a unified categorical framework for deriving various program logics, such as correctness and relational Hoare logic, using imperative categories and an internal language for imperative multicategories.
Contribution
It introduces a novel categorical foundation for program logics based on uniformly traced distributive copy-discard categories and an internal language for imperative multicategories.
Findings
Derived multiple program logics from categorical axioms
Introduced an internal language for imperative multicategories
Provided combinators for Dijkstra's guarded command language
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Algebra and Logic · Logic, Reasoning, and Knowledge · Rough Sets and Fuzzy Logic