Modal quantales, involutive quantales, Dedekind Quantales

Georg Struth 📧 and Cameron Calk

July 25, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Related publications

  • Fahrenberg, U., Johansen, C., Struth, G., & Ziemiański, K. (2023). Catoids and modal convolution algebras. Algebra Universalis, 84(2).
  • Calk, C., Malbos, P., Pous, D., & Struth, G. (2023). Higher Catoids, Higher Quantales and their Correspondences (Version 2). arXiv.

Session Quantales_Converse