论文标题
不一致的连贯性
Incoherent coherences
论文作者
论文摘要
本文探讨了一个通用的框架，包括符合传统抽象代数的签名 - 轴方法的通用框架。确定和抽象的语法操作所需的样板代码被识别出来。一些常见的样板证明也被广泛化。
This article explores a generic framework of well-typed and well-scoped syntaxes, with a signature-axiom approach resembling traditional abstract algebra. The boilerplate code needed in defining operations on syntaxes is identified and abstracted away. Some of the frequent boilerplate proofs are also generalized.
