二阶计算规则的模块化终止性及其在代数效应处理器中的应用
Modular Termination for Second-Order Computation Rules and Application to Algebraic Effect Handlers
AI总结：
提出一种基于语义标注翻译和Blanqui一般模式的模块化终止性证明方法，实现为工具SOL，并成功应用于证明带代数效应处理器的调用-按-值演算变体的终止性。
摘要：
我们提出了一种新的二阶计算模块化终止性证明方法，并报告了其实施工具SOL。该方法对于证明高阶基础演算的终止性非常有用。为建立该方法，我们使用了语义标注翻译的一种变体以及Blanqui的一般模式：一个强规范化的语法判据。作为应用，我们将该方法应用于证明带有代数效应和效应处理器的调用-按-值演算的一个变体的终止性。我们还展示了我们的工具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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
