Reflexive toolbox for regular expression matching
Vladimir Komendantsky · 2012
We study a derivative method allowing to prove termination of computations on regular expressions. A Coq formalisation of a canonical non-deterministic finite automaton construction on a regular expression is presented. The correctness of the functional definitions is formally verified in Coq using the libraries and the small-scale reflection tools of Ssreflect. We propose to extend the proofs further, and this is a work in progress, to study termination of containment and equivalence in terms of partial derivatives. This serves as a major motivation and intended application of the presented approach. A method that we develop in the paper, called shadowing, allows for a smooth program extraction from decision procedures whatever the complexity of the dependently typed proofs.