认证的无上下文解析：Valiant 算法在 Agda 中的形式化
计算机科学中的逻辑
2019-03-14 v2
摘要
Valiant (1975) 提出了一种用于识别上下文无关语言的算法。迄今为止，它仍是为此目的具有最佳渐近复杂度的算法。本文给出了 Valiant 算法的一种推广的代数规范、实现及正确性证明。该推广可用于识别、解析或上三角矩阵传递闭包的一般计算。证明由 Agda 证明助手认证。该认证代表了基于类型论的证明助手中规范和证明的最新方法。因此，本文也可作为 Agda 系统的教程阅读。
引用
@article{arxiv.1601.07724,
title = {Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda},
author = {Jean-Philippe Bernardy and Patrik Jansson},
journal= {arXiv preprint arXiv:1601.07724},
year = {2019}
}