[isabelle] New AFP entry: Kleene Algebra
- To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] New AFP entry: Kleene Algebra
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Wed, 16 Jan 2013 12:59:20 +0100
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130107 Thunderbird/17.0.2
Alasdair Armstrong, Georg Struth, Tjark Weber
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
In the AFP at last!
This archive was generated by a fusion of
Pipermail (Mailman edition) and