论文标题
可变的绑定和替代（无名）假人
Variable binding and substitution for (nameless) dummies
论文作者
论文摘要
通过将De Bruijn代表的众所周知特性与无名假人抽象，我们设计了一种具有可变结合和避免捕获替代的语法理论。我们将其作为Fiore，Plotkin和Turi的方法的更简单替代方法，我们与之建立了牢固的正式联系。我们还表明，我们的理论很容易结合术语之间的简单类型和方程。
By abstracting over well-known properties of De Bruijn's representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi's approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.
