Formalizing Higher-Order Termination in Coq

TL;DR

This paper presents a formalization of higher-order rewriting termination theory in Coq, enabling the implementation and verification of termination techniques with a certified checker.

Contribution

It introduces a formal Coq-based framework for higher-order termination proofs, allowing the implementation and verification of various termination methods.

Findings

Formalization of higher-order rewriting in Coq

Implementation of termination techniques like interpretation and dependency pairs

Extraction of verified termination checkers to OCaml

Abstract

We describe a formalization of higher-order rewriting theory and formally prove that an AFS is strongly normalizing if it can be interpreted in a well-founded domain. To do so, we use Coq, which is a proof assistant based on dependent type theory. Using this formalization, one can implement several termination techniques, like the interpretation method or dependency pairs, and prove their correctness. Those implementations can then be extracted to OCaml, which results in a verified termination checker.