Alasdair Armstrong, Georg Struth, and Tjark Weber. Archive of Formal Proofs, January 2013. Formal proof development.
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, and binary relations form Kleene algebras, and consider further models based on lattices, max-plus semirings and min-plus semirings. We also demonstrate that dioids are closed under the formation of matrices and formal power series (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 middle-layer from which programming applications can quickly be explored, implemented and verified.
The original publication is available at http://afp.sf.net/entries/Kleene_Algebra.shtml.
@article{armstrong13kleene,
author = {Alasdair Armstrong and Georg Struth and Tjark Weber},
title = {{Kleene} Algebra},
journal = {Archive of Formal Proofs},
month = jan,
year = {2013},
note = {\url{http://afp.sf.net/entries/Kleene_Algebra.shtml}, Formal proof development}
}