# Certifying Higher-Order Polynomial Interpretations

## TL;DR

This paper introduces a formal certification method for termination proofs in higher-order rewriting systems using polynomial interpretations, including a tool to verify proofs generated by Wanda within Coq.

## Contribution

It formalizes the polynomial interpretation method for higher-order rewriting and provides a tool to verify Wanda's termination proofs in Coq.

## Key findings

- Formalization of polynomial interpretation for higher-order rewriting
- Development of a tool to verify Wanda's proofs in Coq
- Enhanced reliability of termination proofs verification

## 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.