Report
A Diagrammatic Algebra for Program Logics
| العنوان: | A Diagrammatic Algebra for Program Logics |
|---|---|
| المؤلفون: | Bonchi, Filippo, Di Giorgio, Alessandro, Di Lavore, Elena |
| سنة النشر: | 2024 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Logic in Computer Science |
| الوصف: | Tape diagrams provide a convenient notation for arrows of rig categories, i.e., categories equipped with two monoidal products, $\oplus$ and $\otimes$, where $\otimes$ distributes over $\oplus $. In this work, we extend tape diagrams with traces over $\oplus$ 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 $\otimes$ is a cartesian bicategory, while the one provided by $\oplus$ 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. Comment: arXiv admin note: text overlap with arXiv:2210.09950 |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2410.03561 |
| رقم الانضمام: | edsarx.2410.03561 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |