一句话：提出基于导数的可见下推文法解析器生成器，线性时间产出并提取全部歧义解析树，核心算法在 Coq 中验证。
本文针对可见下推文法（VPG）的识别与解析，提出一种基于导数的函数式解析器生成器。生成的解析器可接受歧义文法，并在线性时间内为输入串构造包含所有合法解析树的解析森林，且每棵解析树也可在线性时间内提取。为支持更灵活的 VPG 形式，作者还给出一个从 tagged CFG 到 VPG 的可靠翻译器，并通过运行翻译后 VPG 解析树中嵌入的语义动作来进一步生成 tagged CFG 的解析树。性能上与 ANTLR、GNU Bison 及流行手写解析器进行比较；核心解析算法的正确性和时间复杂度在 Coq 证明助手中形式化验证。
In this article, we present a derivative-based, functional recognizer and parser generator for visibly pushdown grammars. The generated parser accepts ambiguous grammars and produces a parse forest containing all valid parse trees for an input string in linear time. Each parse tree in the forest can then be extracted also in linear time. Besides the parser generator, to allow more flexible forms of the visibly pushdown grammars, we also present a translator that converts a tagged CFG to a visibly pushdown grammar in a sound way, and the parse trees of the tagged CFG are further produced by running the semantic actions embedded in the parse trees of the translated visibly pushdown grammar. The performance of the parser is compared with popular parsing tools, including ANTLR, GNU Bison, and other popular hand-crafted parsers. The correctness and the time complexity of the core parsing algorithm are formally verified in the proof assistant Coq.
@article{paperbot2135,
title = {A Derivative-based Parser Generator for Visibly Pushdown Grammars},
author = {Xiaodong Jia and Ashish Kumar and Gang Tan},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {2},
year = {2023},
doi = {10.1145/3591472}
}