2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/32167Kleene 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.21 pages, 1 figure; preliminary version appeared in Proc. Workshop on Coalgebraic Methods in Computer Science (CMCS'03)Logic in Computer ScienceProgramming LanguagesF.3.1;I.1.1;I.1.3text