A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests

Todd Schmid; Tobias Kappé; Alexandra Silva

doi:10.1007/978-3-031-30044-8_12

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests

Todd Schmid, Tobias Kappé^*, Alexandra Silva

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

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’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.

Original language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings
Editors	Thomas Wies
Publisher	Springer
Pages	309-336
Number of pages	28
ISBN (Electronic)	978-3-031-30044-8
ISBN (Print)	978-3-031-30043-1
DOIs	https://doi.org/10.1007/978-3-031-30044-8_12
Publication status	Published - 17 Apr 2023
Event	32nd European Symposium on Programming - Paris, France Duration: 22 Apr 2023 → 27 Apr 2023

Publication series

Series	Lecture Notes in Computer Science (LNCS)
Volume	13990
ISSN	0302-9743

Symposium

Symposium	32nd European Symposium on Programming
Abbreviated title	ESOP 2023
Country/Territory	France
City	Paris
Period	22/04/23 → 27/04/23

Access to Document

10.1007/978-3-031-30044-8_12Licence: CC BY

https://arxiv.org/abs/2301.11301Licence: CC BY

Cite this

Schmid, T., Kappé, T., & Silva, A. (2023). A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests. In T. Wies (Ed.), Programming Languages and Systems: 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings (pp. 309-336). Springer. https://doi.org/10.1007/978-3-031-30044-8_12

Schmid, Todd ; Kappé, Tobias ; Silva, Alexandra. / A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests. Programming Languages and Systems: 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings. editor / Thomas Wies. Springer, 2023. pp. 309-336 (Lecture Notes in Computer Science (LNCS), Vol. 13990).

@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",

}

Schmid, T, Kappé, T & Silva, A 2023, A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests. in T Wies (ed.), Programming Languages and Systems: 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings. Springer, Lecture Notes in Computer Science (LNCS), vol. 13990, pp. 309-336, 32nd European Symposium on Programming, Paris, France, 22/04/23. https://doi.org/10.1007/978-3-031-30044-8_12

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests. / Schmid, Todd; Kappé, Tobias; Silva, Alexandra.
Programming Languages and Systems: 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings. ed. / Thomas Wies. Springer, 2023. p. 309-336 (Lecture Notes in Computer Science (LNCS), Vol. 13990).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests

AU - Schmid, Todd

AU - Kappé, Tobias

AU - Silva, Alexandra

PY - 2023/4/17

Y1 - 2023/4/17

N2 - 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’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.

AB - 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’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.

U2 - 10.1007/978-3-031-30044-8_12

DO - 10.1007/978-3-031-30044-8_12

M3 - Conference Article in proceeding

SN - 978-3-031-30043-1

T3 - Lecture Notes in Computer Science (LNCS)

SP - 309

EP - 336

BT - Programming Languages and Systems

A2 - Wies, Thomas

PB - Springer

T2 - 32nd European Symposium on Programming

Y2 - 22 April 2023 through 27 April 2023

ER -

Schmid T, Kappé T, Silva A. A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests. In Wies T, editor, Programming Languages and Systems: 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings. Springer. 2023. p. 309-336. (Lecture Notes in Computer Science (LNCS), Vol. 13990). doi: 10.1007/978-3-031-30044-8_12

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests

Abstract

Publication series

Symposium

Access to Document

Fingerprint

Cite this