@inproceedings{ed1be95d26f34642bd7486d7aeab4891,

title = "A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests",

abstract = "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 to KAT, GKAT does not have an algebraic axiomatization, but relies on an analogue of Salomaa{\textquoteright}s axiomatization of Kleene Algebra. In this paper, we present an algebraic axiomatization and prove two completeness results for a large fragment of GKAT consisting of skip-free programs.",

author = "Todd Schmid and Tobias Kapp{\'e} and Alexandra Silva",

year = "2023",

month = apr,

day = "17",

doi = "10.1007/978-3-031-30044-8_12",

language = "English",

isbn = "978-3-031-30043-1",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "309--336",

editor = "Thomas Wies",

booktitle = "Programming Languages and Systems",

note = "32nd European Symposium on Programming, ESOP 2023 ; Conference date: 22-04-2023 Through 27-04-2023",

}