J.-C. Filliātre. Finite Automata Theory in Coq: A constructive proof of Kleene's theorem. Research Report 97-04, LIP - ENS Lyon, February 1997.

We describe here a development in the system Coq of a piece of Finite Automata Theory. The main result is the Kleene's theorem, expressing that regular expressions and finite automata define the same languages. From a constructive proof of this result, we automatically obtain a functional program that compiles any regular expression into a finite automata, which constitutes the main part of the implementation of grep-like programs. This functional program is obtained by the automatic method of extraction which removes the logical parts of the proof to keep only its informative contents. Starting with an idea of what we would have written in ML, we write the specification and do the proofs in such a way that we obtain the expected program, which is therefore efficient.

[ bib | .ps.Z ]

Back