关于正则表达式的证明 [英] proofs about regular expressions

问题描述

有人知道以下示例吗？

1. 关于正则表达式（可能使用反向引用）（例如 Coq ）。


2. 以依赖类型的语言（例如 Agda >）有关正则表达式。

1. Proof developments about regular expressions (possibly extended with backreferences) in proof assistants (such as Coq).
2. Programs in dependently-typed languages (such as Agda) about regular expressions.

推荐答案

使用从属类型的经过认证的编程有一节介绍如何创建经过验证的正则表达式匹配器。 Coq贡献者具有自动机贡献可能会有用。 Jan-Oliver Kaiser为其单身汉论文。

Certified Programming with Dependent Types has a section on creating a verified regular expression matcher. Coq Contribs has an automata contribution that might be useful. Jan-Oliver Kaiser formalized the equivalence between regular expressions, finite automata and the Myhill-Nerode characterization in Coq for his bachelors thesis.

这篇关于关于正则表达式的证明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！