A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
复制标题
DOI：
10.1145/3236785
复制
发表时间：
2018-09-01
影响因子：
1.8
通讯作者：
McKinna, James
中科院分区：
文献类型：
--
作者：
Allais, Guillaume;Atkey, Robert;McKinna, James
几乎每种编程语言的语法都包含绑定和相应绑定出现的概念，以及相应的等价、捕获避免替换、类型上下文、运行时环境等概念。在过去，对编程语言的实现和推理需要小心处理，以维护绑定变量的正确行为。现代编程语言包括一些特性，这些特性支持用类型来表示约束，比如作用域安全。尽管如此，程序员仍然被迫为每个范围安全操作的新实现（例如，重命名、替换、去糖、打印等）重新编写相同的样板文件，然后再次编写正确性证明。我们提出了一个具有绑定的语法表达范围，并演示了如何(1)通过泛型编程一劳永逸地实现范围安全遍历；(2)如何通过泛型证明推导出这些遍历的性质。我们的宇宙描述，一般遍历和证明，以及我们的例子都已经在Agda中形式化了，并且可以在附带的材料中获得。
Almost every programming language's syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of a-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.