[isabelle] New in the AFP: Kleene Algebras with Domain

Iâm happy to announce another AFP entry, adding to our already substantial coverage of Kleene Algebras, and incidentally the 12th contribution of 2016.


Many thanks for this development!

Larry Paulson

> Kleene Algebras with Domain
> Kleene algebras with domain are Kleene algebras endowed with an operation that maps each element of the algebra to its domain of definition (or its complement) in abstract fashion. They form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics. We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations in Isabelle/HOL that ranges from domain and antidomain semigroups to modal Kleene algebras and divergence Kleene algebras. We link these algebras with models of binary relations and program traces. We include some examples from modal logics, termination and program analysis.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.