@inproceedings{6555a84244434085a75cd2d71faceee1,
title = "Certification of proving termination of term rewriting by matrix interpretations",
abstract = "We develop a Coq formalization of the matrix interpretation method, which is a recently developed, powerful approach to proving termination of term rewriting. Our formalization is a contribution to the CoLoR project and allows to automatically certify matrix interpretation proofs produced by tools for proving termination. Thanks to this development the combination of CoLoR and our tool, TPA, was the winner in 2007 in the new certified category of the annual Termination Competition.",
author = "A. Koprowski and H. Zantema",
year = "2008",
doi = "10.1007/978-3-540-77566-9\_28",
language = "English",
isbn = "978-3-540-77565-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "328--339",
editor = "V. Geffert and J. Karhum{\"a}ki and A. Bertoni and B. Preneel and P. N{\'a}vrat and M. Bielikov{\'a}",
booktitle = "SOFSEM 2008 : Theory and Practice of Computer Science (Proceedings 34th Conference, Nov{\'y} Smokovec, Slovakia, January 19-25, 2008)",
address = "Germany",
}