License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2016.22
URN: urn:nbn:de:0030-drops-64379
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6437/
Go to the corresponding LIPIcs Volume Portal

Brunet, Paul ; Pous, Damien

A Formal Exploration of Nominal Kleene Algebra

pdf-format:
LIPIcs-MFCS-2016-22.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{brunet_et_al:LIPIcs:2016:6437,
  author =	{Paul Brunet and Damien Pous},
  title =	{{A Formal Exploration of Nominal Kleene Algebra}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{22:1--22:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Piotr Faliszewski and Anca Muscholl and Rolf Niedermeier},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6437},
  URN =		{urn:nbn:de:0030-drops-64379},
  doi =		{10.4230/LIPIcs.MFCS.2016.22},
  annote =	{Keywords: Nominal sets, Kleene algebra, equational theory, Coq}
}

Keywords: Nominal sets, Kleene algebra, equational theory, Coq
Collection: 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)
Issue Date: 2016
Date of publication: 19.08.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI