A Coalgebraic Approach to Kleene Algebra with Tests
Chen, Hubie · Pucella, Riccardo
Original · EN
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.
English translation
This paper has no Arabic translation yet. Be the first: it takes a few seconds, and the result is stored for every future reader.