KAT + B!

Niels Bjørn Bugge Grathwohl; Dexter Kozen; Konstantinos Mamouras

doi:10.1145/2603088.2603095

KAT + B!

Niels Bjørn Bugge Grathwohl, Dexter Kozen, Konstantinos Mamouras

Datalogisk Institut

9 Citationer (Scopus)

Abstract

It is known that certain program transformations require a small amount of mutable state, a feature not explicitly provided by Kleene algebra with tests (KAT). In this paper we show how to axiomatically extend KAT with this extra feature in the form of mutable tests. The extension is conservative and is formulated as a general commutative coproduct construction. We give several results on deductive completeness and complexity of the system, as well as some examples of its use.

Originalsprog	Engelsk
Titel	CSL-LICS '14 : Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Antal sider	10
Forlag	Association for Computing Machinery
Publikationsdato	2014
Artikelnummer	44
ISBN (Trykt)	978-1-4503-2886-9
DOI	https://doi.org/10.1145/2603088.2603095
Status	Udgivet - 2014
Begivenhed	CSL-LICS '14 - Vienna, Østrig Varighed: 14 jul. 2014 → 18 jul. 2014

Konference

Konference	CSL-LICS '14
Land/Område	Østrig
By	Vienna
Periode	14/07/2014 → 18/07/2014

Adgang til dokumentet

10.1145/2603088.2603095

KAT + B!Forlagets udgivne version, 346 KB

Citationsformater

KAT + B! / Grathwohl, Niels Bjørn Bugge; Kozen, Dexter; Mamouras, Konstantinos.

CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . Association for Computing Machinery, 2014. 44.

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Grathwohl, NBB, Kozen, D & Mamouras, K 2014, KAT + B! i CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) ., 44, Association for Computing Machinery, CSL-LICS '14, Vienna, Østrig, 14/07/2014. https://doi.org/10.1145/2603088.2603095

@inproceedings{1ea3610a2256414d8724080e9fffba6a,

title = "KAT + B!",

abstract = "It is known that certain program transformations require a small amount of mutable state, a feature not explicitly provided by Kleene algebra with tests (KAT). In this paper we show how to axiomatically extend KAT with this extra feature in the form of mutable tests. The extension is conservative and is formulated as a general commutative coproduct construction. We give several results on deductive completeness and complexity of the system, as well as some examples of its use.",

author = "Grathwohl, {Niels Bj{\o}rn Bugge} and Dexter Kozen and Konstantinos Mamouras",

year = "2014",

doi = "10.1145/2603088.2603095",

language = "English",

isbn = "978-1-4503-2886-9",

booktitle = "CSL-LICS '14",

publisher = "Association for Computing Machinery",

note = "CSL-LICS '14 ; Conference date: 14-07-2014 Through 18-07-2014",

}

TY - GEN

T1 - KAT + B!

AU - Grathwohl, Niels Bjørn Bugge

AU - Kozen, Dexter

AU - Mamouras, Konstantinos

PY - 2014

Y1 - 2014

N2 - It is known that certain program transformations require a small amount of mutable state, a feature not explicitly provided by Kleene algebra with tests (KAT). In this paper we show how to axiomatically extend KAT with this extra feature in the form of mutable tests. The extension is conservative and is formulated as a general commutative coproduct construction. We give several results on deductive completeness and complexity of the system, as well as some examples of its use.

AB - It is known that certain program transformations require a small amount of mutable state, a feature not explicitly provided by Kleene algebra with tests (KAT). In this paper we show how to axiomatically extend KAT with this extra feature in the form of mutable tests. The extension is conservative and is formulated as a general commutative coproduct construction. We give several results on deductive completeness and complexity of the system, as well as some examples of its use.

U2 - 10.1145/2603088.2603095

DO - 10.1145/2603088.2603095

M3 - Article in proceedings

SN - 978-1-4503-2886-9

BT - CSL-LICS '14

PB - Association for Computing Machinery

T2 - CSL-LICS '14

Y2 - 14 July 2014 through 18 July 2014

ER -

KAT + B!

Abstract

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater