Certifying Higher-Order Polynomial Interpretations
Abstract
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.
Cite
@article{arxiv.2302.11892,
title = {Certifying Higher-Order Polynomial Interpretations},
author = {Niels van der Weide and Deivid Vale and Cynthia Kop},
journal= {arXiv preprint arXiv:2302.11892},
year = {2023}
}
Comments
This new version fixes typos in the introduction, adds a reference to the published version, and adds the \hideLipics command so the temporary lipics logo isn't shown. No textual content was added or removed in this version