Formalizing the Kleene Star for Square Matrices
Teo Asplund · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2014
This thesis gives a formal description of the Kleene star for square matrices over a Kleene algebra. It builds on previous work on Kleene algebras and their formal description in Isabelle/HOL, and is a step toward a formal proof that square matrices over a Kleene algebra form a Kleene algebra.