Certification of Termination Proofs Using Polynomial Interpretations

The aim of the work described in this paper is to formalize in the proof assistant \coq the polynomial interpretation termination criterion, and to describe how a termination proof for a given rewriting system can be built automatically by using this formalization together with a polynomial interpretation provided by the CiME tool. The main results of this work are a formalization of first-order term algebras (with arities), a formalization of polynomials with several indeterminates, and a formalized proof of the polynomial interpretation termination criterion