2026-08-16T23:49:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18405 2024-03-06T11:01:49Z ddc:004 open_access

Certifying Higher-Order Polynomial Interpretations van der Weide, Niels Vale, Deivid Kop, Cynthia higher-order rewriting Coq termination formalization 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 that is used to prove termination, namely the polynomial interpretation method. In addition, we give a program that processes proof traces containing a high-level description of a termination proof into a formal Coq proof script that can be checked by Coq. We demonstrate the usability of this approach by certifying higher-order polynomial interpretation proofs produced by Wanda, a termination analysis tool for higher-order rewriting. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Niels van der Weide and Deivid Vale and Cynthia Kop 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.30 urn:nbn:de:0030-drops-184051 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.30 eng https://creativecommons.org/licenses/by/4.0/legalcode