Formally verifying the properties of formal systems using a proof assistant requires justifying numerous minor lemmas about capture-avoiding substitution. Despite work on category-theoretic accounts of syntax and variable binding, raw, first-order representations of syntax, the kind considered by many practitioners and compiler frontends, have received relatively little attention. Therefore applications miss out on the benefits of category theory, most notably the promise of reusing formalized infrastructural lemmas between implementations of different systems. Our Coq framework Tealeaves provides libraries of reusable infrastructure for a raw, locally nameless representation and can be extended to other representations in a modular fashion. In this paper we give a string-diagrammatic account of decorated traversable monads (DTMs), the key abstraction implemented by Tealeaves. We define DTMs as monoids of structured endofunctors before proving a representation theorem a la Kleisli, yielding a recursion combinator for finitary tree-like datatypes.

翻译：使用证明助手形式化验证形式系统的性质，需要证明大量关于避免捕获替换的辅助引理。尽管已有关于语法和变量绑定的范畴论解释的研究，但许多实践者和编译器前端所考虑的原始一阶语法表示却相对较少受到关注。因此，相关应用未能充分受益于范畴论的优势，尤其是不同系统实现之间可复用形式化基础设施引理的前景。我们的 Coq 框架 Tealeaves 提供了用于原始局部无名表示的可复用基础设施库，并可通过模块化方式扩展至其他表示。本文给出了装饰可遍历单子（DTM）的字符串图解解释——这是 Tealeaves 的核心抽象。我们将 DTM 定义为结构化自函子的幺半群，进而证明了类 Kleisli 表示定理，为有限树状数据类型推导出递归组合子。