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.

翻译：高阶重写是一个框架，可用于编写高阶程序并研究其性质。其中一种性质是终止性：即对于所有输入，程序最终都会停止执行并产生输出。目前已开发出多种工具来检查高阶重写系统是否具有终止性。然而，开发此类工具难度较大且容易出错。本文提出了一种认证高阶项重写系统终止性证明的方法。我们形式化了一个特定方法——多项式解释法，用于证明终止性。此外，我们开发了一个程序，将高阶重写系统终止性分析工具Wanda的输出转化为Coq脚本，从而能够检查该输出是否为有效的终止性证明。