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. The library is written in the proof assistant Coq and basically ready to be used with the programming languages Ocaml and Haskell supported by Coq.
An important outcome of this project is our understanding of the feasibility and possible time estimates of the more general and more fundamental work plan available at http://yeslogic.com/kingdom/. We have addressed some of the concrete issues underlying this large work plan, namely, proof methodologies for standard regular expressions and finite automata. We studied the legacy of Stephen C. Kleene and some other prominent researchers of the golden age of automata theory such as Victor Glushkov as well as recent research reports. What we have attempted to achieve in this project was to connect their legacy with today's software practices.
