Skip to Main content Skip to Navigation
Conference papers

Certification of Termination Proofs Using Polynomial Interpretations

Sébastien Hinderer 1
1 LANGUE ET DIALOGUE - Human-machine dialogue with a significant language component
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Agnès Vidard <>
Submitted on : Wednesday, April 5, 2006 - 2:43:35 PM
Last modification on : Friday, February 26, 2021 - 3:28:04 PM


  • HAL Id : inria-00001205, version 1



Sébastien Hinderer. Certification of Termination Proofs Using Polynomial Interpretations. 17th European Summer School in Logic, Language and Information - ESSLLI '05, Aug 2005, Edimbourg/Grande Bretagne. ⟨inria-00001205⟩



Record views