一句话：提出二阶代数理论下证明等式理论可判定性的通用方法，并实现 Haskell 分析器 SOL。
本文研究编程语言概念中等式理论的可判定性证明问题。作者在二阶代数理论框架下提出一套通用方法论，将二阶计算的语法结果与语义结果以非平凡方式结合并扩展，用于证明由二阶代数理论导出的计算规则具有合流性与强规范化。为此实现了基于 Haskell 的分析工具 Second-Order Laboratory（SOL）。论文用多个文献中的代数理论验证该方法，包括 monad 与 λ-演算的等式理论、Plotkin 和 Power 的状态与比特理论、Stark 的 π-演算理论，并展示了该方法如何解决 monoidal category 的 coherence 问题。
Abstract We present a general methodology of proving the decidability of equational theory of programming language concepts in the framework of second-order algebraic theories. We propose a Haskell-based analysis tool, i.e. Second-Order Laboratory, which assists the proofs of confluence and strong normalisation of computation rules derived from second-order algebraic theories. To cover various examples in programming language theory, we combine and extend both syntactical and semantical results of the second-order computation in a non-trivial manner. We demonstrate how to prove decidability of various algebraic theories in the literature. It includes the equational theories of monad and λ-calculi, Plotkin and Power’s theory of states and bits, and Stark’s theory of π-calculus. We also demonstrate how this methodology can solve the coherence of monoidal categories.