proofs about regular expressions

Question

Does anyone know any examples of the following?

1. Proof developments about regular expressions (possibly extended with backreferences) in proof assistants (such as Coq).
2. Programs in dependently-typed languages (such as Agda) about regular expressions.

Answer 1

Moreira, Pereira & de Sousa, On the Mechanisation of Kleene Algebra in Coq gives a nice verified construction of the Antimirov derivative of regexps in Coq. It's pretty easy to read off a CFA from this construction, and to compute the intersection of regexps.

I'm not sure why you separate Coq from dependently typed programming: Coq essentially is programming in a polymorphic dependently typed lambda calculus with inductive types (i.e., CIC, the calculus of inductive constructions).

I've never heard of a formalisation of regexps in a dependently typed language, nor have I heard of something such as an Antimirov-like derivative for regexps with backtracking, but Becchi & Crowley, Extending Finite Automata to Efficiently Match Perl-Compatible Regular Expressions provide a notion of finite-state automata that matches a Perl-like regexp languages. That might attractive to formalisers in the near future.

Answer 2

I don't know of any development that treats regular expressions by themselves.

Finite automata, however, relevant since NFAs are the standard way to match those regular expressions, have been studied in NuPRL. Have a look at : Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe. Constructively Formalizing Automata Theory.

Should you be interested in approaching those formal languages through algebra, esp. developing finite semigroup theory, there are a number of algebra libraries developed in various theorem provers that you could think of using, with one particularly efficient in a finite setting.

Answer 3

See Perl Regular Expression Matching is NP-Hard

Regex matching is NP-hard when regexes are allowed to have backreferences.

Reduction of 3-CNF-SAT to Perl Regular Expression Matching

[...] 3-CNF-SAT is NP-complete. If there were an efficient (polynomial-time) algorithm for computing whether or not a regex matched a certain string, we could use it to quickly compute solutions to the 3-CNF-SAT problem, and, by extension, to the knapsack problem, the travelling salesman problem, etc. etc.

Answer 4

The proof assistant Isabelle/HOL ships a number of formalized proofs regarding regular expressions (without back reference): http://afp.sourceforge.net/browser_info/devel/HOL/Regular-Sets/

(here is a paper by the authors regarding what they did exactly).

Another approach is to characterize regular expressions via Myhill-Nerode Theorem: http://www.dcs.kcl.ac.uk/staff/urbanc/Publications/itp-11.pdf

Answer 5

Certified Programming with Dependent Types has a section on creating a verified regular expression matcher. Coq Contribs has an automata contribution that might be useful. Jan-Oliver Kaiser formalized the equivalence between regular expressions, finite automata and the Myhill-Nerode characterization in Coq for his bachelors thesis.