正则表达式 – 关于正则表达式的证明

发布时间：2020-12-14 06:36:13 所属栏目：百科来源：网络整理

导读：有没有人知道以下的例子？证明助理(如Coq)的有关regular expressions(可能延长至backreferences)的证明发展。有关正则表达式的依赖类型语言(如Agda)的程序。 Certified Programming with Dependent Types有一个创建验证的正则表达式匹配器的部分。 Coq Con

有没有人知道以下的例子？

>证明助理(如Coq)的有关regular expressions(可能延长至backreferences)的证明发展。
>有关正则表达式的依赖类型语言(如Agda)的程序。

Certified Programming with Dependent Types有一个创建验证的正则表达式匹配器的部分。 Coq Contribs有一个 automata contribution可能是有用的。 Jan-Oliver Kaiser正式表达了正则表达式，有限自动机和Coq中的Myhill-Nerode表征之间的等价性为他的 bachelors thesis。

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!