具有绑定的语法之类型与作用域安全宇宙：其语义与证明

几乎每种编程语言的语法都包含绑定器及相应绑定出现的概念，以及伴随而来的 $\alpha$-等价、避免捕获的替换、类型上下文、运行时环境等概念。过去，实现和推理编程语言需要谨慎处理以维持绑定变量的正确行为。现代编程语言包含能使作用域安全等约束在类型中表达的特性。然而，程序员仍被迫为每个作用域安全操作（例如重命名、替换、脱糖、打印等）的新实现反复编写相同的样板代码，并再次为正确性证明重写。我们提出一个具有绑定的富有表达力的语法宇宙，并展示如何（1）通过泛型编程一次性实现作用域安全遍历；以及（2）如何通过泛型证明推导这些遍历的性质。我们的宇宙描述、泛型遍历与证明，以及示例均已用 Agda 形式化，并可在 https://github.com/gallais/generic-syntax 的配套材料中获取。