### 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

- Computer science/Semantics and reasoning
- Mathematics/Algebra
- Mathematics/Order

### 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

### Depends on

- Kleene Algebras with Domain
- Kleene Algebra
- Quantales

### Used by

- Catoids, Categories, Groupoids

## Cite

×

Quantales_Converse-AFP

    @article{Quantales_Converse-AFP,
      author  = {Georg Struth and Cameron Calk},
      title   = {Modal quantales, involutive quantales, Dedekind Quantales},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Quantales_Converse.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Aug 10, 2023 : Isabelle2022