正则表达式的证明

有人知道下面的例子吗

  1. 在证明助手(如Coq)中关于正则表达式(可能扩展为反向引用)的证明开发
  2. 使用依赖类型语言(如Agda)编写的关于正则表达式的程序

具有依赖类型的认证编程有一节介绍如何创建经验证的正则表达式匹配器。Coq Contribs有一个自动机贡献,这可能很有用。Jan Oliver Kaiser在其学士学位论文中,在Coq中形式化了正则表达式、有限自动机和Myhill-Nerode特征之间的等价性

发表评论