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…