Nominal sets, automata and bracket algebra
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
html
relation-algebra @ 2d9066e
.gitignore
.gitmodules
LICENSE.md
Makefile
Makefile.local
README.md
_CoqProject
aeq_facts.v
algebra.v
alphaKA.v
alpha_delta.v
alpha_derivatives.v
alpha_regexp.v
alternate_eq.v
atoms.v
automata.v
bijection.v
binding_finite.v
closed_automaton.v
closed_languages.v
completenessKA.v
equiv_stacks.v
factors.v
filters.v
language.v
nominalsetoid.v
normalise.v
positive_regexp.v
regexp.v
representative.v
splits.v
stacks.v
strict_split.v
subword.v
systems.v
tools.v
traces.v
transducer.v
tri_split.v
words.v

README.md

BracketAlgebra

Nominal sets, automata and bracket algebra

This repository contains 🐔Coq🐔 libraries dealing 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

To obtain this library, 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.