License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.30
URN: urn:nbn:de:0030-drops-184051
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18405/
van der Weide, Niels ;
Vale, Deivid ;
Kop, Cynthia
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 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.
BibTeX - Entry
@InProceedings{vanderweide_et_al:LIPIcs.ITP.2023.30,
author = {van der Weide, Niels and Vale, Deivid and Kop, Cynthia},
title = {{Certifying Higher-Order Polynomial Interpretations}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {30:1--30:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18405},
URN = {urn:nbn:de:0030-drops-184051},
doi = {10.4230/LIPIcs.ITP.2023.30},
annote = {Keywords: higher-order rewriting, Coq, termination, formalization}
}
