一句话：提出 de Bruijn 无名哑元的变量绑定与捕获避免替换新理论，并建立其与 Fiore–Plotkin–Turi 方法的强形式联系。
变量绑定与捕获避免替换是编程语言语法的核心问题。既有工作常用 de Bruijn 的无名哑元表示，或 Fiore、Plotkin 与 Turi 的抽象范畴论方法。本文通过抽象 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.
@article{paperbot2773,
title = {Variable binding and substitution for (nameless) dummies},
author = {André Hirschowitz and Tom Hirschowitz and Ambroise Lafont and Marco Maggesi},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 1},
year = {2024},
doi = {10.46298/lmcs-20(1:18)2024}
}