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.

BibTeX

@inproceedings{RT-Isabelle12,
  author    = "Ren{\'e} Thiemann",
  title     = "Towards the Certification of Complexity Proofs",
  booktitle = "Isabelle Users Workshop 2012",
  editor    = "Tobias Nipkow and Larry Paulson and Makarius Wenzel",
  year      = 2012,
  note      = "\url{http://arxiv.org/abs/1208.1609}"
}