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 |
[-] |
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.
@techreport{brunet18-2019, title="Bracket Algebra, a nominal theory of interleaved scopes", author={Brunet, Paul and Petrişan, Daniela and Silva, Alexandra}, year={2019}, institution={}, }
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, title="A Kleene theorem for nominal automata", author={Brunet, Paul and Silva, Alexandra}, year={2019}, booktitle={ICALP}, doi={"10.4230/LIPIcs.ICALP.2019.107"}, }
Talks |
[-] |
Documents |
[-] |
Bracket Algebra, a nominal theory of interleaved scopes | |
draft | |
A Kleene theorem for nominal automata | |
draft | |
BracketAlgebra Coq library | |
github repository |