Modal Quantales, Involutive Quantales, Dedekind Quantales

Georg Struth 📧 and Cameron Calk

July 25, 2023

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

BSD 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 1). arXiv. https://doi.org/10.48550/ARXIV.2307.09253

Session Quantales_Converse