{"a", "b", "c"}* = {ε, "a", "b", "c", "aa", "ab", "ac", "ba", "bb", "bc", "ca", "cb", "cc", ...}.
The Kleene star can be defined not just for regular expressions and languages, but also in many other contexts where a notion of iteration is available. In particular, iterated matrix multiplication gives rise to a definition of the Kleene star for square matrices.
In this project, you will formalize the Kleene star for matrices in the interactive proof assistant Isabelle. You will translate the textbook definition of the Kleene star into a precise (machine-readable) definition and give detailed (machine-checkable) proofs of its most important properties.
This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.