Bracket Algebra

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.


This library is available as a Github repository:

To downlaod it directly, simply run the command:

git clone  --recurse-submodules

Notice the --recurse-submodules, which is necessary to get the submodule relation-algebra, due to Damien Pous.


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


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:


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

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.

   title="Bracket Algebra, a nominal theory of interleaved scopes",
   author={Brunet, Paul and Petrişan, Daniela and Silva, Alexandra}
A Kleene theorem for nominal automata. (2019)

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.

   title="A Kleene theorem for nominal automata",
   author={Brunet, Paul and Silva, Alexandra}


Bracket Algebra
Highlights, Berlin, September 2018