Regular Expression Equivalence

We formalize a unified framework for verified decision procedures for regular expression equivalence. Five recently published formaliza-tions of such decision procedures (three based on derivatives, two on marked regular expressions) can be obtained as instances of the frame-work. We discover that the two approaches based on marked regular expressions, which were previously thought to be the same, are dif-ferent, and one seems to produce uniformly smaller automata. The common framework makes it possible to compare the performance of the different decision procedures in a meaningful way