一句话：提出一个类型与作用域安全的带绑定语法宇宙，可泛型实现遍历并泛型证明其性质。
编程语言语法普遍包含绑定结构及其绑定出现，涉及 α 等价、避免捕获替换、类型上下文、运行时环境等概念。过去实现和推理语言时需小心维护绑定变量行为，且每个作用域安全操作（重命名、替换、脱糖、打印等）及其正确性证明都要重复编写样板。本文提出一个表达力强的“带绑定语法宇宙”，通过泛型编程一次性实现作用域安全遍历，并通过泛型证明派生这些遍历的性质。该宇宙描述、泛型遍历与证明以及示例均已在 Agda 中形式化。
Almost every programming language’s syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of α-equivalence, capture avoiding substitution, typing contexts, runtime environments, and so on. In the past, implementing and reasoning about programming languages required careful handling to maintain the correct behaviour of bound variables. Modern programming languages include features that enable constraints like scope safety to be expressed in types. Nevertheless, the programmer is still forced to write the same boilerplate over again for each new implementation of a scope safe operation (e.g., renaming, substitution, desugaring, printing, etc.), and then again for correctness proofs. We present an expressive universe of syntaxes with binding and demonstrate how to (1) implement scope safe traversals once and for all by generic programming; and (2) how to derive properties of these traversals by generic proving. Our universe description, generic traversals and proofs, and our examples have all been formalised in Agda and are available in the accompanying material. NB. we recommend printing the paper in colour to benefit from syntax highlighting in code fragments.
@article{paperbot291,
title = {A type and scope safe universe of syntaxes with binding: their semantics and proofs},
author = {Guillaume Allais and Robert Atkey and James Chapman and Conor McBride and James McKinna},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236785}
}