一句话：提出用有界自然函子统一建模带绑定语法，并在 Isabelle/HOL 中形式化自由变量、α-等价与捕获避免替换等原理。
本文提出一个用于规约和推理带绑定语法的通用框架。它将抽象绑定类型建模为集合上的一族函子，并提供若干操作，以模块化方式构造复杂绑定模式和绑定感知数据类型，支持非良基与无限分支类型。该框架不限定具体语法格式，但仍足够具体，可定义自由变量、α-等价和捕获避免替换等基本项算子，以及相应的定义与推理原则。该工作与经典高阶逻辑兼容，并已在证明助手 Isabelle/HOL 中形式化。
We present a general framework for specifying and reasoning about syntax with bindings. Abstract binder types are modeled using a universe of functors on sets, subject to a number of operations that can be used to construct complex binding patterns and binding-aware datatypes, including non-well-founded and infinitely branching types, in a modular fashion. Despite not committing to any syntactic format, the framework is ``concrete'' enough to provide definitions of the fundamental operators on terms (free variables, alpha-equivalence, and capture-avoiding substitution) and reasoning and definition principles. This work is compatible with classical higher-order logic and has been formalized in the proof assistant Isabelle/HOL.
@article{paperbot654,
title = {Bindings as bounded natural functors},
author = {Jasmin Christian Blanchette and Lorenzo Gheri and Andrei Popescu and Dmitriy Traytel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290335}
}