Kleene Algebra
Tobias Kapp\'e, Alexandra Silva, Jana Wagemaker

TL;DR
This paper introduces Kleene Algebra, a formal system for reasoning about program equivalences using regular expressions, automata, and algebraic laws, with educational exercises and an optional automata theory chapter.
Contribution
It provides an accessible introduction to Kleene Algebra, linking regular expressions, automata, and algebraic proofs of program equivalence, including coalgebra perspectives.
Findings
Equivalence of regular expressions can be proved using KA laws
Automata theory can be developed through coalgebra approach
Kleene Algebra provides a sound framework for program equivalence reasoning
Abstract
This booklet serves as an introduction to Kleene Algebra (KA), a set of laws that can be used to study general equivalences between programs. It discusses how general programs can be modeled using regular expressions, how those expressions correspond to automata, and how this correspondence can be exploited to obtain the central result of KA, namely that an equivalence of regular expressions is true if and only if it can be proved using the laws of KA. Each chapter closes with a set of exercises to further build intuition and understanding, and there is an optional chapter that develops automata theory through the lens of coalgebra.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
