A formal exploration of nominal Kleene algebra
An axiomatisation of Nominal Kleene Algebra has been proposed by Gabbay and Ciancia, and then shown to be complete and decidable by Kozen et al. However, one can think of at least four different formulations for a Kleene Algebra with names: using freshness conditions or a presheaf structure (types), and with explicit permutations or not. We formally show that these variations are all equivalent. Then we introduce an extension of Nominal Kleene Algebra, motivated by relational models of programming languages. The idea is to let letters (i.e., atomic programs) carry a set of names, rather than being reduced to a single name. We formally show that this extension is at least as expressive as the original one, and that it may be presented with or without a presheaf structure, and with or without syntactic permutations. Whether this extension is strictly more expressive remains open. All our results were formally checked using the Coq proof assistant.
Related talks | ||
|
A Kleene Theorem for Nominal Automata
ICALP
in Patras,
July 2019
.
|
More | |
|
Bracket Algebra
Highlights
in Berlin,
September 2018
.
|
More | |
|
A formal exploration of Nominal Kleene Algebra
MFCS
in Krakow,
August 2016
.
|
More | |
Related papers | ||
|
Bracket Algebra, a nominal theory of interleaved scopes
(2019)
with Alexandra Silva and Daniela Petrişan. |
More | |
|
A Kleene theorem for nominal automata
(in ICALP 2019)
with Alexandra Silva. |
More | |
| Algebras of relations: from algorithms to formal proofs (in Université de Lyon 2016) | More | |