一句话：提出依赖 Lambek 演算，用线性类型内在验证解析器只产生合法语法树，并编码正则/上下文无关文法与自动机。
本文提出依赖 Lambek 演算（Lambek D），一种用于可验证解析与形式文法理论的领域特定依赖类型理论。其核心思想是以线性类型作为形式文法的语法，解析器写成线性项；线性类型限制提供内在验证，保证解析器对输入串只产生合法解析树。作者用归纳线性类型与对非线性数据的依赖编码正则文法、上下文无关文法及多种自动机轨迹，并据此定义基于确定自动机的正则表达式解析器与上下文无关文法解析器实例。论文给出指称语义，将线性类型解释为从字符串到抽象解析树集合的函数，将项解释为解析变换器；并基于该语义在 Agda 中用浅嵌入实现原型，所有示例解析器均已实现。
We present Dependent Lambek Calculus (Lambek D ), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek D , linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars. We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek D using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.
@article{paperbot3080,
title = {Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus},
author = {Steven Schaefer and Nathan Varner and Pedro Henrique Azevedo de Amorim and Max S. New},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729281}
}