A Coalgebraic Approach to Kleene Algebra with Tests
<|reference_start|>A Coalgebraic Approach to Kleene Algebra with Tests: 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.<|reference_end|>
@article{chen2004a,
    title={A Coalgebraic Approach to Kleene Algebra with Tests},
    author={Hubie Chen, Riccardo Pucella},
    journal={Theoretical Computer Science, 327 (1-2), 23-44 (2004)},
    year={2004},
    archivePrefix={arXiv},
    eprint={cs/0405097},
    primaryClass={cs.LO cs.PL}
}