Nominal Kleene Algebra
Coq files and Documentation
This proof is decomposed in a number of modules, dealing with
module contains simple notations, definitions, tactics and
lemmas, mostly independant of the rest of the developpement.
simply define atoms, and permutations of atoms.
library defines a number of operations on lists of atoms.
an equivalence relation on lists of atoms.
of expressions is defined, together with some elementary
functions such as size, equality...
define in this library some predicates over expressions,
such as typing, freshness...
important functions manipulating expressions can be found
this library the generic proof system is defined, as well as
the various axiom bundles.
technical proofs dealing with bridges between positive and
technical proofs dealing with bridges between typed and
technical proofs dealing with bridges between theories with
our without explicit permutations.
of the different theories, and stability results about them.
technical proofs dealing with bridges from atomic to
of the preorder relations on theories, and proofs of the
ordering of our theories.
The other files are still in a preliminary state.