Abstract
This AFP entry provides mathematical components for modal quantales,
involutive quantales and Dedekind quantales. Modal quantales are
simple extensions of modal Kleene algebras useful for the
verification of recursive programs. Involutive quantales appear in
the study of C*-algebras. Dedekind quantales are relatives of
Tarski's relation algebras, hence relevant to program verification
and beyond that to higher rewriting. We also provide
components for weaker variants such as Kleene algebras with converse
and modal Kleene algebras with converse.
License
Topics
Related publications
- Fahrenberg, U., Johansen, C., Struth, G., & Ziemiański, K. (2023). Catoids and modal convolution algebras. Algebra Universalis, 84(2). https://doi.org/10.1007/s00012-023-00805-9
- Calk, C., Malbos, P., Pous, D., & Struth, G. (2023). Higher Catoids, Higher Quantales and their Correspondences (Version 2). arXiv. https://doi.org/10.48550/ARXIV.2307.09253
Session Quantales_Converse
- Modal_Kleene_Algebra_Var
- Kleene_Algebra_Converse
- Modal_Kleene_Algebra_Converse
- Modal_Quantale
- Quantale_Converse