Towards the Certification of Complexity Proofs

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.

Isabelle Users Workshop 2012, Associated with ITP 2012, http://www4.in.tum.de/~nipkow/Isabelle2012/