cl-banner

Certifying Exact Complexity Bounds for Matrix Interpretations

Jose Divasón, Sebastiaan Joosten, Ondrej Kuncar, René Thiemann, and Akihisa Yamada

Proceedings of the 16th International Workshop on Logic and Computational Complexity (LCC 2016),   pp. 4 – 7, 2016.

Abstract

CeTA is a tool — whose correctness is formally proven in Isabelle/HOL — that certifies complexity proofs generated by untrusted complexity analyzers. We present our recent developments in CeTA that enables certifying exact complexity bounds for matrix interpretations. We formalized a number of important results in linear algebra, as well as an implementation of algebraic numbers.

 

  PDF

BibTeX 

@inproceedings{JDSJOKRTAY16lcc,
author = "Jose Divas{\'o}n and Sebastiaan Joosten and Ond{\v r}ej Kun{\v c}ar and
Ren{\'e} Thiemann and Akihisa Yamada",
title = "Certifying Exact Complexity Bounds for Matrix Interpretations",
booktitle = "Proceedings of the 16th International Workshop on Logic and Computational Complexity",
pages = {4--7},
year = 2016
}
Nach oben scrollen