UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

A formal exploration of Nominal Kleene Algebra

Brunet, P; Pous, D; (2016) A formal exploration of Nominal Kleene Algebra. In: (Proceedings) 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Dagstuhl Publishing Green open access

[img]
Preview
Text
LIPIcs-MFCS-2016-22.pdf - ["content_typename_Published version" not defined]

Download (536kB) | Preview

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.

Type: Proceedings paper
Title: A formal exploration of Nominal Kleene Algebra
Event: 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)
ISBN-13: 9783959770163
Open access status: An open access version is available from UCL Discovery
DOI: 10.4230/LIPIcs.MFCS.2016.22
Publisher version: https://doi.org/10.4230/LIPIcs.MFCS.2016.22
Language: English
Additional information: This work is licensed under a Creative Commons Attribution 4.0 International License. The images or other third party material in this article are included in the article’s Creative Commons license, unless indicated otherwise in the credit line; if the material is not included under the Creative Commons license, users will need to obtain permission from the license holder to reproduce the material. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/
UCL classification: UCL > Provost and Vice Provost Offices
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: http://discovery.ucl.ac.uk/id/eprint/10053757
Downloads since deposit
8Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item