论文标题
对避免捕获替代，上下文应用，命名替代，部分分化等的语法结构定义的统一处理
A unified treatment of structural definitions on syntax for capture-avoiding substitution, context application, named substitution, partial differentiation, and so on
论文作者
论文摘要
我们介绍了具有辅助功能的语法的类别，称为AndissiblemonAd形态。然后，我们依靠结构递归的抽象形式，然后设计通用工具来构建基本数据的可允许的单片形态。 这些工具可自动化无处不在的标准模式（1）在连续的，潜在的依赖性层中定义辅助功能，以及（2）通过诱导在语法上证明辅助函数的特性。 我们介绍了来自thelitration的重要例子，包括带有避免capture替代的标准lambda-calculus，一种具有结合评估环境的lambda-calculus，带有命名取代的lambda-mu-calculus，命名为取代和差异lambda-calculus。
We introduce a category-theoreticabstraction of a syntax with auxiliary functions, called an admissiblemonad morphism. Relying on an abstract form of structural recursion,we then design generic tools to construct admissible monad morphismsfrom basic data. These tools automate ubiquitous standard patternslike (1) defining auxiliary functions in successive, potentiallydependent layers, and (2) proving properties of auxiliary functions byinduction on syntax. We cover significant examples from theliterature, including the standard lambda-calculus withcapture-avoiding substitution, a lambda-calculus with bindingevaluation contexts, the lambda-mu-calculus with named substitution, andthe differential lambda-calculus.
