A Coalgebraic Approach to Kleene Algebra with Tests
Hubie Chen, Riccardo Pucella

TL;DR
This paper develops a coalgebraic framework for Kleene algebra with tests, introducing new automata-theoretic interpretations and a coinductive proof principle to reason about program equivalences.
Contribution
It presents a novel coalgebraic approach to Kleene algebra with tests, including a new automata interpretation and a coinductive proof method.
Findings
Established a coalgebraic theory for Kleene algebra with tests
Introduced a new automata-theoretic interpretation
Developed a coinductive proof principle for expression equivalence
Abstract
Kleene algebra with tests is an extension of Kleene algebra, the algebra of regular expressions, which can be used to reason about programs. We develop a coalgebraic theory of Kleene algebra with tests, along the lines of the coalgebraic theory of regular expressions based on deterministic automata. Since the known automata-theoretic presentation of Kleene algebra with tests does not lend itself to a coalgebraic theory, we define a new interpretation of Kleene algebra with tests expressions and a corresponding automata-theoretic presentation. One outcome of the theory is a coinductive proof principle, that can be used to establish equivalence of our Kleene algebra with tests expressions.
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
Topicssemigroups and automata theory · Logic, programming, and type systems · Formal Methods in Verification
