1 CoLoR: a Coq Library on Rewriting and termination
Frédéric Blanqui, Solange Coupet-Grimal, William Delobel, Sébastien Hinderer, Adam Koprowski, A. Geser, H. Sondergaard · 2006
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.