认证高阶多项式解释
Certifying Higher-Order Polynomial Interpretations
AI总结：
本文提出一种认证高阶项重写系统终止性证明的方法，通过形式化多项式解释方法，并将终止性分析工具Wanda的输出转换为Coq脚本以验证证明的有效性。
摘要：
高阶重写是一个可以编写高阶程序并研究其性质的框架。其中一个性质是终止性：即对于所有输入，程序最终停止执行并产生输出的情况。已经开发了几种工具来检查高阶重写系统是否终止。然而，开发此类工具很困难且容易出错。在本文中，我们提出了一种认证高阶项重写系统终止性证明的方法。我们形式化了一种特定的方法，即用于证明终止性的多项式解释方法。此外，我们提供了一个程序，将高阶重写系统终止性分析工具Wanda的输出转换为Coq脚本，以便我们检查该输出是否为有效的终止性证明。
英文摘要：
Higher-order rewriting is a framework in which one can write higher-order programs and study their properties. One such property is termination: the situation that for all inputs, the program eventually halts its execution and produces an output. Several tools have been developed to check whether higher-order rewriting systems are terminating. However, developing such tools is difficult and can be error-prone. In this paper, we present a way of certifying termination proofs of higher-order term rewriting systems. We formalize a specific method, namely the polynomial interpretation method, that is used to prove termination. In addition, we give a program that turns the output of Wanda, a termination analysis tool for higher-order rewriting systems, into a Coq script, so that we can check whether the output is a valid proof of termination.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
