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.

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

expand/reduce
Bracket Algebra, a nominal theory of interleaved scopes. (2019)
Paul Brunet, Daniela Petrişan and Alexandra Silva. Submitted in ESOP.
Abstract

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

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

expand/reduce
c Bracket Algebra [slides]
Highlights, September 2018

Documents

expand/reduce