A one-year project on languages, automata and regular expressions started in October '08. It has been sponsored by YesLogic Ltd and is due to completion in September '09. The project has materialised in a library for creation of certified regular expression software.
Old web page
Submitted by vladimir on 29 August, 2009 - 11:33Here is my old web page that I keep to commemorate my 18-month postdoc experience in INRIA Sophia Antipolis and for other biographical reasons.
Regular expresion library
Submitted by vladimir on 29 August, 2009 - 10:47The 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:
