Finite Automata Theory in Coq
A constructive proof of Kleene's theorem


Abstract:

We describe here a development in the Coq proof assistant 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.

A research report is available. Get it. BibTeX.


Source of the development

The whole Coq development will be soon available from this page.

Computational meaning of the proof

From the constructive proof of this theorem, we automatically obtain a certified Caml program (which realizes the specification). To get more details about the process of extraction in the Coq system, you may have a look at the documentation (available by FTP with the system) : Execution of extracted programs in Caml and Gofer. Here is the program we obtain :

The Caml program extracted from the proof

Test of the extracted program

In order to test the extracted program, we first define some pretty-printers for various types, to make the results easier to read (file test.ml). Here are the results for the following regular expressions:

Compilation of a regular expression
Regular expressionCaml codeAutomaton (PS file)
b* session1.ml A1
ab* session2.ml A2
ab*+b session3.ml A3


Homepage Français
Jean-Christophe Filliâtre (formatted with yamlpp).