Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2507.18238 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915408090497024 |
|---|---|
| author | Bonchi, Filippo Di Lavore, Elena Román, Mario Staton, Sam |
| author_facet | Bonchi, Filippo Di Lavore, Elena Román, Mario Staton, Sam |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_18238 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Program Logics via Distributive Monoidal Categories Bonchi, Filippo Di Lavore, Elena Román, Mario Staton, Sam Logic in Computer Science 18M50 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. |
| title | Program Logics via Distributive Monoidal Categories |
| topic | Logic in Computer Science 18M50 |
| url | https://arxiv.org/abs/2507.18238 |