2 papers
cs.FL2026
An Elementary Proof of the FMP for Kleene Algebra
Tobias Kappé
Kleene Algebra (KA) is a useful tool for proving that two programs are equivalent. Because KA's equational theory is decidable, it integrates well with interactive theorem provers.…
cs.LO2024
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Tobias Kappé, Todd Schmid, Alexandra Silva
Guarded Kleene Algebra with Tests (GKAT) is a fragment of Kleene Algebra with Tests (KAT) that was recently introduced to reason efficiently about imperative programs. In contrast…