有人知道下面的例子吗
- 在证明助手(如Coq)中关于正则表达式(可能扩展为反向引用)的证明开发
- 使用依赖类型语言(如Agda)编写的关于正则表达式的程序
具有依赖类型的认证编程有一节介绍如何创建经验证的正则表达式匹配器。Coq Contribs有一个自动机贡献,这可能很有用。Jan Oliver Kaiser在其学士学位论文中,在Coq中形式化了正则表达式、有限自动机和Myhill-Nerode特征之间的等价性
共同学习, 共同进步, 祝各位早日成为代码大神
有人知道下面的例子吗
具有依赖类型的认证编程有一节介绍如何创建经验证的正则表达式匹配器。Coq Contribs有一个自动机贡献,这可能很有用。Jan Oliver Kaiser在其学士学位论文中,在Coq中形式化了正则表达式、有限自动机和Myhill-Nerode特征之间的等价性