1 CoLoR: a Coq Library on Rewriting and termination

Abstract. Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs. Termination is an important and difficult problem. Many criteria have been developed over the last years. They are more and more complex and applied on larger and larger systems. For these tools to be used in the certification of critical systems and proof assistants, their results must be certified