有没有人知道以下的例子？
>证明助理(如Coq)的有关regular expressions(可能延长至backreferences)的证明发展。
>有关正则表达式的依赖类型语言(如Agda)的程序。
Certified Programming with Dependent Types有一个创建验证的正则表达式匹配器的部分。
Coq Contribs有一个
automata contribution可能是有用的。 Jan-Oliver Kaiser正式表达了正则表达式，有限自动机和Coq中的Myhill-Nerode表征之间的等价性为他的
bachelors thesis。
