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.

翻译：我们为二阶计算提出了新的模块化验证终止方法,并报告了其实施 SOL。证明方法对证明高阶基础计算计算终止有用。为了确定方法,我们使用了语义标签翻译和Blanqui的General Schema的变异版本和Blanqui的General Schema:强度正常化的综合标准。作为一种应用,我们使用这种方法来显示具有代数效果和效果处理器的调用-旁-普什值微积分变式的终止。我们还表明,我们的SOL工具能够有效解决更高排序终止问题。