一句话：提出用二阶代数理论证明演算等式理论可判定的通用方法，并实现 Haskell 工具 SOL 辅助合流性与强规范化证明。
论文研究编程语言演算中等式理论的可判定性证明问题。作者在二阶代数理论框架下提出一种通用方法，将计算规则转化为重写系统，并结合与扩展二阶计算的语法和语义结果，证明其合流性与强规范化，从而导出等式理论可判定。为此实现 Haskell 分析工具 SOL，辅助此类证明。案例涵盖单子与 λ 演算、Plotkin 与 Power 的状态理论以及 Stark 的 π 演算等，展示了该方法在多种语言理论中的实用性。
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 SOL, 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 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 lambda-calculi, Plotkin and Power's theory of states, and Stark's theory of pi-calculus.
@article{Hamana17,
title = {How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation},
author = {Makoto Hamana},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110266}
}