An executable regular expression (regexp) matcher as defined in the paper Proof-directed debugging revisited, proved correct in the Coq proof assistant.
Definitions and proofs:
Executable matcher:
OCaml 4.02.3(or later)menhirOCamlbuildocamlfind
One easy way to install the dependencies (ssreflect, RegLang, and menhir) is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install menhir coq-mathcomp-ssreflect coq-reglang
Then, run make. This will compile the Coq syntax and relation definitions along with the proofs and functions, and extract OCaml code.
To build the executable matcher program, run make matcher.