A diagrammatic algebra for program logics

DOI10.1007/978-3-031-90897-2_15MaRDI QIDQ6889881zbMATH OpenFDO

Authors Filippo Bonchi, Alessandro di Giorgio, Elena di Lavore

Publication date 4 December 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-90897-2_15

zbMATH Keywords

Cartesian bicategoriesprogram logicsrig categories

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Cites work

• A completeness theorem for Kleene algebras and the algebra of regular events
• A Finite Axiomatisation of Finite-State Automata Using String Diagrams
• A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
• A survey of graphical languages for monoidal categories
• An axiomatic basis for computer programming
• Bicategories of processes
• Cartesian bicategories. I
• Coalgebras and cartesian categories
• Connector algebras, Petri nets, and BIP
• Diagrammatic algebra of first order logic
• Feedback and generalized logic
• Full abstraction for signal flow graphs
• FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
• Generic weakest precondition semantics from monads enriched with order
• Graphical affine algebra
• Graphical Conjunctive Queries.
• Hoare Logic in the Abstract
• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 2125662 (Why is no real title available?)
• scientific article; zbMATH DE number 3385869 (Why is no real title available?)
• Interacting quantum observables: categorical algebra and diagrammatics
• Introduction to linear bicategories
• Kleene algebra with converse
• Notes on equational theories of relations
• On Hoare logic and Kleene algebra with tests
• On the positive calculus of relations with transitive closure
• Simple relational correctness proofs for static analyses and program transformations
• String diagrams for regular logic (extended abstract)
• The geometry of tensor calculus. I
• The relational machine calculus
• The uniformity principle on traced monoidal categories
• The ZX-calculus is complete for stabilizer quantum mechanics
• Traced monoidal categories
• Two roads to classicality
• Weakest preconditions in fibrations
• What are the meaning and the purpose of numbers?

Cited in

(2)

• Compositional separation of control flow and data flow
• Tapes as stochastic matrices of string diagrams

This page was built for publication: A diagrammatic algebra for program logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6889881)