一句话：提出二阶计算规则的模块化终止证明方法并实现工具SOL，用于代数效应处理器的CBPV演算终止性。
高阶或二阶计算规则的终止性证明通常难以模块化扩展，尤其涉及代数效应与效应处理器的基元演算。本文提出一种新的二阶计算终止性模块化证明方法，并实现工具SOL。该方法融合语义标注翻译的变体与Blanqui的General Schema，即强规范化的语法判据，从而将二阶规则转化为可由语法判据处理的形式。作为应用，作者证明了带代数效应和效应处理器的call-by-push-value演算变体终止。实验表明，SOL能有效求解高阶终止问题。
We present a new modular proof method of termination for second-order computation, and report its implementation SOL. The proof method is useful for proving termination of higher-order foundational calculi. To establish the method, we use a variation of semantic labelling translation and Blanqui's General Schema: a syntactic criterion of strong normalisation. As an application, we apply this method to show termination of a variant of call-by-push-value calculus with algebraic effects and effect handlers. We also show that our tool SOL is effective to solve higher-order termination problems.
@article{paperbot1692,
title = {Modular Termination for Second-Order Computation Rules and Application to Algebraic Effect Handlers},
author = {Makoto Hamana},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 2},
year = {2022},
doi = {10.46298/lmcs-18(2:18)2022}
}