##
A Formalisation of the Myhill-Nerode Theorem using Regular Expressions only

### Christian Urban

There are numerous textbooks on regular languages. Many of them focus
on finite automata for proving properties. Unfortunately, automata
are not so straightforward to formalise in theorem provers. The reason
is that natural representations for automata are graphs, matrices or
functions, none of which are inductive datatypes. Regular expressions
can be defined straightforwardly as a datatype and a corresponding
reasoning infrastructure comes for free in theorem provers. I will
show that most parts of formal language theory, including the
Myhill-Nerode Theorem, can be formalised using only regular expressions.
The central notions in this work are derivatives and partial derivatives
of regular expressions.