Email Gateway (Aug 10 2023 at 15:30): Email Gateway (Aug 10 2023 at 15:30):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to report a new entry:
Modal Quantales, Involutive Quantales, Dedekind Quantales, by Georg Struth and Cameron Calk
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.
Now online at https://www.isa-afp.org/entries/Quantales_Converse.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC