RIS.tools: Toolbox of simple definitions, lemmas and tactics.

RIS.atoms: Nominal sets.

RIS.bijection: generate permutations.

RIS.nominalsetoid: Nominal sets up-to equivalence.

RIS.words: words, binding monoid and alpha-equivalence.

RIS.stacks: an algebra of stacks.

RIS.transducer: definition and properties of the binding transducer.

RIS.equiv_stacks: dynamic properties of the binding transducer.

RIS.alternate_eq: equivalent definitions of alpha-equivalence.

RIS.traces: extracting stacks directly from words.

RIS.representative: generic representation of nominal sets.

RIS.normalise: normal form for words up-to alpha-equivalence.

RIS.factors: square bindings and binding division.

RIS.algebra: algebraic structures.

RIS.language: Languages.

RIS.regexp: regular expressions and the free Kleene algebra.

RIS.completenessKA: Link with relation-algebra to import the completeness proof of Kleene algebra.

RIS.automata: finite state automata.

RIS.systems: affine systems of equations

RIS.positive_regexp: regular expressions that do not contain the empty word.

RIS.subword: the subword ordering on words.

RIS.aeq_facts: lemmas about α-equivalence and the equivalence transducer.


RIS.alphaKA: axiomatisation of regular languages up-to α-equivalence.

RIS.closed_languages: languages closed by α-equivalence.

RIS.binding_finite: binding-finite and memory-finite expressions.

RIS.closed_automaton: computing an automaton for the α-closure of an expression.

This page has been generated by coqdoc