Towards the Certification of Complexity Proofs
Logic in Computer Science
2012-08-09 v1
Abstract
We report on our formalization of matrix-interpretation in Isabelle/HOL. Matrices are required to certify termination proofs and we wish to utilize them for complexity proofs, too. For the latter aim, only basic methods have already been integrated, and we discuss some upcoming problems which arise when formalizing more complicated results on matrix-interpretations, which are based on Cayley-Hamilton's theorem or joint-spectral radius theory.
Keywords
Cite
@article{arxiv.1208.1609,
title = {Towards the Certification of Complexity Proofs},
author = {René Thiemann},
journal= {arXiv preprint arXiv:1208.1609},
year = {2012}
}
Comments
Isabelle Users Workshop 2012, Associated with ITP 2012, http://www4.in.tum.de/~nipkow/Isabelle2012/