一个类型和作用域安全的带约束的语法域：语义和证明
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
摘要：
几乎每一种编程语言的语法都包含绑定器和相应的绑定事件的概念，以及伴随的$α$等价、避免捕获的替换、类型上下文、运行时环境等概念。在过去，实现和推理程序设计语言需要仔细处理以维护绑定变量的正确行为。现代程序设计语言包含了一些特性，这些特性使得像范围安全这样的约束可以用类型来表达。尽管如此，程序员仍然被迫为范围安全操作的每个新实现重新编写相同的样板（例如，重命名、取代、脱糖、印刷等），然后再进行正确性证明。我们提出了一个具有约束力的语法表达宇宙，并演示了如何（1）实现范围安全遍历一劳永逸的泛型编程;（2）如何派生这些遍历的属性泛型证明。我们的宇宙描述，一般的遍历和证明，以及我们的例子都已经在Agda中正式化，并且可以在https://github.com/gallais/generic-syntax在线获得的附带材料中获得。
英文摘要：
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 available online at https://github.com/gallais/generic-syntax.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
