| Certification of Matrix Interpretations in Coq |  |
Abstract:
We describe how to certify the matrix interpretations method for proving termination of term rewriting in the theorem
prover Coq. Certification requires both formalization of the underlying theory of monotone algebras and their instantiation
to vectors and matrices as they are used in the matrix method; as well as a mechanism to deal with concrete examples,
based on those theoretical results.
Certification of Matrix Interpretations in Coq
In
Proceedings of the 9th International Workshop on Termination
( WST '07),
Paris, France.
BibTeX:@inproceedings{mint-cert-WST-07,
author = {Adam Koprowski and Hans Zantema},
title = {Certification of Matrix Interpretations in {Coq}},
booktitle = {Proceedings of the 9th International Workshop on Termination (WST '07)},
year = {2007},
pages = {9--12},
} | 
