A fresh look at programming with names and binders
A fresh look at programming with names and binders
复制标题
重新审视名称和活页夹编程
DOI：
10.1145/1863543.1863575
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
F. Pottier
中科院分区：
文献类型：
--
作者：
N. Pouillard;F. Pottier
包括编译器和定理掠夺在内的各种计算机程序操纵涉及名称和绑定的数据结构。但是，允许以安全自然风格执行这些操作的编程成语的设计在很大程度上仍然难以捉摸。
在本文中，我们提出了一种解决问题的新方法。我们的建议可以被视为编程语言设计或库：实际上，它目前是在AGDA内实施的。它提供了一种安全且表现力的手段，以使用名称和粘合剂进行编程。它足以支持多个具体实现：我们以名义风格介绍一个，并以de bruijn风格呈现。我们使用逻辑关系来证明“良好的程序不会与不同的范围混合名称”。我们在系统中展示了PITTS风格的名义术语的足够编码。
A wide range of computer programs, including compilers and theorem provers, manipulate data structures that involve names and binding. However, the design of programming idioms which allow performing these manipulations in a safe and natural style has, to a large extent, remained elusive.
In this paper, we present a novel approach to the problem. Our proposal can be viewed either as a programming language design or as a library: in fact, it is currently implemented within Agda. It provides a safe and expressive means of programming with names and binders. It is abstract enough to support multiple concrete implementations: we present one in nominal style and one in de Bruijn style. We use logical relations to prove that "well-typed programs do not mix names with different scope". We exhibit an adequate encoding of Pitts-style nominal terms into our system.