| 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.
Certification of Proving Termination of Term Rewriting by Matrix Interpretations
In
Proceedings of the 34th International Conference on Current Trends in Theory and Practice of Computer Science
( SOFSEM '08),
Nový Smokovec, Slovakia.
BibTeX:@inproceedings{mint-cert-SOFSEM-08,
author = {Adam Koprowski and Hans Zantema},
title = {Certification of Proving Termination of Term Rewriting by Matrix Interpretations},
booktitle = {Proceedings of the 34th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM '08)},
year = {2008},
series = {Lecture Notes in Computer Science},
volume = {4910},
pages = {328--339},
} | 
