The regular expression library is written in Coq and available for free download here: http://similare.org/regexp-nfa.tgz. This is still a work in progress that goes through lots of updates and fixes. It is possible that in the future we might choose to release the library in a more systematic way on this site (e.g., keep old revisions).
The library is partly documented in these short papers:
[1] Michael Day and Vladimir Komendantsky. A compiler of regular expressions to NFAs. May 2009. Submitted. PDF
[2] Vladimir Komendantsky. Case analysis on a dependently typed fixed point for regular languages. July 2009. Submitted. PDF
