Kozen, D;
Mamouras, K;
Silva, A;
(2017)
Completeness and incompleteness in nominal Kleene algebra.
Journal of Logical and Algebraic Methods in Programming
, 91
pp. 17-32.
10.1016/j.jlamp.2017.06.002.
Preview |
Text
Silva_NKA.pdf - Accepted Version Download (222kB) | Preview |
Abstract
Gabbay and Ciancia (2011) presented a nominal extension of Kleene algebra as a framework for trace semantics with statically scoped allocation of resources, along with a semantics consisting of nominal languages. They also provided an axiomatization that captures the behavior of the scoping operator and its interaction with the Kleene algebra operators and proved soundness over nominal languages. In this paper, we show that the axioms proposed by Gabbay and Ciancia are not complete over the semantic interpretation they propose. We then identify a slightly wider class of language models over which they are sound and complete.
| Type: | Article |
|---|---|
| Title: | Completeness and incompleteness in nominal Kleene algebra |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1016/j.jlamp.2017.06.002 |
| Publisher version: | https://doi.org/10.1016/j.jlamp.2017.06.002 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Kleene algebra, Nominal sets, Programming logic |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10117572 |
Archive Staff Only
 |
View Item |
