*Nominal sets, automata and bracket algebra*

This Coq librariy deals with nominal sets and regular expressions. It is focused towards **Bracket Algebra**, a style of nominal Kleene algebra well suited for modelling imperative programs.

## Download |

This library is available as a Github repository: https://github.com/monstrencage/BracketAlgebra.

To downlaod it directly, simply run the command:

`git clone --recurse-submodules git@github.com:monstrencage/BracketAlgebra.git`

Notice the `--recurse-submodules`

, which is necessary to get the submodule `relation-algebra`

, due to Damien Pous.

## Compiling |

This library was compiled using:

To compile it, one needs to first compile `relation-algebra`

, then the main library. To compile everything and produce the html documentation, run the following command from the main folder:

`cd relation-algebra && make && cd .. && make gallinahtml`

## Documentation |

The documentation of the library was generated using the utility `coqdoc`

, avalaible as standard in Coq distributions.

A copy of the documentation is here. Other documents of interest for the project are listed below:

## Papers |

Bracket Algebra, a nominal theory of interleaved scopes.
(2019)

Paul Brunet, Daniela Petrişan and Alexandra Silva. Submitted in ESOP.
*Abstract*

Paul Brunet, Daniela Petrişan and Alexandra Silva. Submitted in ESOP.

In this paper we present bracket algebra, a nominal framework that can be used in reasoning about programs with interleaved scopes. We construct a hierarchy of languages based on their memory and binding power. We present a decision procedure for program equivalence and containment for a large class of programs.

@inproceedings{brunet18-2019, booktitle={ESOP}, title="Bracket Algebra, a nominal theory of interleaved scopes", year={2019}, note={submitted}, author={Brunet, Paul and Petrişan, Daniela and Silva, Alexandra} }

A Kleene theorem for nominal automata.
(2019)

Paul Brunet, Alexandra Silva. Submitted in FoSSaCS.
*Abstract*

Paul Brunet, Alexandra Silva. Submitted in FoSSaCS.

Nominal automata are a widely studied class of automata designed to recognise languages over infinite alphabets. In this paper, we present a Kleene theorem for nominal automata by providing a syntax to denote regular nominal languages. We use regular expressions with explicit binders for creation and destruction of names and pinpoint an exact property of these expressions – namely memory-finiteness – that identifies a subclass of expressions denoting exactly egular nominal languages.

@inproceedings{brunet17-2019, booktitle={FoSSaCS}, title="A Kleene theorem for nominal automata", year={2019}, note={submitted}, author={Brunet, Paul and Silva, Alexandra} }

## Talks |

Bracket Algebra | [slides] | |

Highlights, September 2018 |

## Documents |