语法的良好作用域局部无名表示
计算机科学中的逻辑
2026-05-12 v1
摘要
在使用基于依赖类型论的交互式定理证明器来定义和推理涉及绑定构造的语言时，我们主张使用局部无名表示方法的良好作用域版本来表示语法。本文描述了参数化由 Plotkin 风格绑定签名的通用代码，用于该语法表示方法中的 Agda 定理证明器中，给出其对朴素命名语法在 alpha 转换下的充分性证明，并讨论其用例。
引用
@article{arxiv.2605.08990,
title = {Well-Scoped Locally Nameless Representation of Syntax},
author = {Andrew M. Pitts},
journal= {arXiv preprint arXiv:2605.08990},
year = {2026}
}
备注
20 pages, 3 figures