
Kleene
Algebra
Title: 
Kleene Algebra 
Authors:

Alasdair Armstrong,
Georg Struth (g /dot/ struth /at/ sheffield /dot/ ac /dot/ uk) and
Tjark Weber (tjark /dot/ weber /at/ it /dot/ uu /dot/ se)

Submission date: 
20130115 
Abstract: 
These files contain a formalisation of variants of Kleene algebras and
their most important models as axiomatic type classes in Isabelle/HOL.
Kleene algebras are foundational structures in computing with
applications ranging from automata and language theory to computational
modeling, program construction and verification.
We start with formalising dioids, which are additively idempotent
semirings, and expand them by axiomatisations of the Kleene star for
finite iteration and an omega operation for infinite iteration. We
show that powersets over a given monoid, (regular) languages, sets of
paths in a graph, sets of computation traces, binary relations and
formal power series form Kleene algebras, and consider further models
based on lattices, maxplus semirings and minplus semirings. We also
demonstrate that dioids are closed under the formation of matrices
(proofs for Kleene algebras remain to be completed).
On the one hand we have aimed at a reference formalisation of variants
of Kleene algebras that covers a wide range of variants and the core
theorems in a structured and modular way and provides readable proofs
at text book level. On the other hand, we intend to use this algebraic
hierarchy and its models as a generic algebraic middlelayer from which
programming applications can quickly be explored, implemented and verified. 
BibTeX: 
@article{Kleene_AlgebraAFP,
author = {Alasdair Armstrong and Georg Struth and Tjark Weber},
title = {Kleene Algebra},
journal = {Archive of Formal Proofs},
month = jan,
year = 2013,
note = {\url{http://isaafp.org/entries/Kleene_Algebra.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Used by: 
KAD, KAT_and_DRA, Multirelations, Regular_Algebras, Relation_Algebra, Residuated_Lattices 
