Towards the Certification of Complexity Proofs
Ren\'e Thiemann
TL;DR
This paper discusses formalizing matrix-interpretations in Isabelle/HOL to certify termination and complexity proofs, highlighting current capabilities and challenges in formalizing advanced mathematical results for complexity analysis.
Contribution
It presents the formalization of matrix-interpretations in Isabelle/HOL for termination and complexity proofs, and discusses challenges in extending to advanced mathematical methods.
Findings
Basic matrix-interpretation methods are integrated into Isabelle/HOL.
Formalization of complex results like Cayley-Hamilton theorem is ongoing.
Identifies challenges in formalizing joint-spectral radius theory for 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Advanced Algebra and Logic