HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Wednesday, April 5, 2006 - 2:43:35 PM
Last modification on : Friday, February 4, 2022 - 3:34:48 AM


  • 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