regex - 关于正则表达式的证明

标签 regex types proof coq agda

有人知道以下任何示例吗？

  • 在证明助手(例如regular expressions)中有关backreferences(可能已通过Coq扩展)的证明开发。
  • 以依赖类型的语言(例如Agda)编写有关正则表达式的程序。

    • 最佳答案

    Certified Programming with Dependent Types有一节介绍如何创建经过验证的正则表达式匹配器。 Coq Contribs具有一个可能有用的automata contribution。 Jan-Oliver Kaiser在Coq中为其bachelors thesis形式化了正则表达式，有限自动机和Myhill-Nerode表征之间的等价关系。

    关于regex - 关于正则表达式的证明，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/897595/

    上一篇：time - Lua中数字的最大值是多少？

    下一篇：ruby-on-rails - 使用Rails验证助手:message，但不希望在消息中列出列名

    相关文章：

    c++ - 用户定义类型的隐式类型转换

    php - Mysql返回具有正确数据类型的数组

    math - 为什么程序不能被证明？

    formula - (N–1) + (N–2) + (N–3) + ... + 1= N*(N–1)/2 的证明是什么

    python - 版本号大于 1.18.10 的正则表达式

    C++ 表达式模板——为什么是基类？

    python - 如何在 Python 中简洁地级联多个正则表达式语句

    haskell - 使用类型系统检查输出与输入列表的长度

    java - 从字符串中删除 HTML 标记

    python - 如何使 sklearn.TfidfVectorizer 标记特殊短语？

    ©2024 IT工具网  联系我们