Regular expressions are mostly known as pattern matching expressions in scripting languages (Perl, sed, awk, etc.). They are also theoretically studied for their strong relationship with Automata Theory. A regular expression denote a language (set of words) and two regular expressions are equivalent when they denote the same language. The equivalence problem is decidable and furthermore, any equivalence can be proved axiomatically. Various such axiomatisations have flourished during the last fifty years, we will survey the most important ones.
Every axiomatisation come together with a proof of completeness of the following form: if two regular expressions are equivalent then there exists proof within the axiomatic system. In principle, when this completeness proof is constructive one can extract from it an algorithm that produces a certificate of the equivalence. We have filled the gap developping a program (written in OCaml) that computes certificates. For this purpose we have designed a domain specific proof system with a language of commands for composing a certificate checkable within this system (this is a joint work with Bodhayan Roy).
