View article

These theory files are only sparsely commented. Additional information on the hierarchy of Kleene algebras and its formalisation in Isabelle/HOL can be found in a tutorial paper [12] or an overview article [16]. While these papers focus on the automation of algebraic reasoning, the present formalisation presents readable proofs whenever these are interesting and instructive.

Expansions of the hierarchy to modal Kleene algebras and Hoare logics as well as infinitary and higher-order Kleene algebras [15, 1], and an alternative hierarchy of regular algebras and Kleene algebras [11]—orthogonal to the present one—have also been implemented. These are not covered by this repository.