A Formal Exploration of Nominal Kleene Algebra

Authors Paul Brunet, Damien Pous

Thumbnail PDF


  • Filesize: 0.51 MB
  • 13 pages

Document Identifiers

Author Details

Paul Brunet
Damien Pous

Cite AsGet BibTex

Paul Brunet and Damien Pous. A Formal Exploration of Nominal Kleene Algebra. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 22:1-22:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


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.
  • Nominal sets
  • Kleene algebra
  • equational theory
  • Coq


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Paul Brunet. Web appendix to this abstract, 2016. URL: http://perso.ens-lyon.fr/paul.brunet/nka.
  2. Murdoch Gabbay and Andrew Pitts. A new approach to abstract syntax involving binders. In Logic in Computer Science, 1999. Proceedings. 14th Symposium on, pages 214-224. IEEE, 1999. Google Scholar
  3. Murdoch James Gabbay and Vincenzo Ciancia. Freshness and name-restriction in sets of traces with names. In Foundations of Software Science and Computational Structures, FoSSaCS 2011, pages 365-380. Springer, 2011. Google Scholar
  4. Dexter Kozen. Kleene algebra with tests. Transactions on Programming Languages and Systems, 19(3):427-443, May 1997. URL: http://dx.doi.org/10.1145/256167.256195.
  5. Dexter Kozen, Konstantinos Mamouras, Daniela Petrisan, and Alexandra Silva. Nominal Kleene Coalgebra. In Automata, Languages, and Programming, ICALP 2015, pages 286-298. Springer, 2015. Google Scholar
  6. Dexter Kozen, Konstantinos Mamouras, and Alexandra Silva. Completeness and incompleteness in Nominal Kleene Algebra. In Relational and Algebraic Methods in Computer Science, RAMiCS 2015, pages 51-66. Springer, 2015. Google Scholar
  7. Andrew M Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57. Cambridge University Press, 2013. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail