A regular expression toolkit

Various constructions on regular expressions and finite automata are nice to contemplate, but hard to describe informally without sinking in a mire of nested subscripts, and hard to implement in a conventional way without becoming lost in a maze of twisty little pointers, all alike. The goal in this project is to come up with a perspicuous implementation of some of these algorithms in a suitable programming language such as Haskell or OCaml, abstracting shared patterns such as fixpoint computations as higher-order functions. A suitable target would be a program for marking Models of Computation homework: it would accept two regular expressions on the command line, and either verify that they were equivalent or print a word that matched one expression but not the other. More ambitious would be a program that could also prove the equivalence from the Kozen axioms.