验证高阶多项式解释
摘要：高阶重写是一个框架，可以编写高阶程序并研究其性质。其中一个性质是终止性：即对于所有输入，程序最终停止执行并产生输出。已经开发了几种工具来检查高阶重写系统的终止性。然而，开发这样的工具是困难且容易出错的。在本文中，我们提出了一种认证高阶术语重写系统终止性证明的方法。我们将一种特定方法-多项式解释方法形式化，用于证明终止性。此外，我们还提供了一个程序，将高阶重写系统的终止分析工具Wanda的输出转化为Coq脚本，以便我们可以检查输出是否是终止性的有效证明。
作者：Niels van der Weide, Deivid Vale, Cynthia Kop
论文ID：2302.11892
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-08