cl-banner

Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs

Christian Sternagel and René Thiemann

Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), Lecture Notes in Computer Science 8560, pp. 441 – 455, 2014.

Abstract

Monotone algebras are frequently used to generate reduction orders in automated termination and complexity proofs. To be able to certify these proofs, we formalized several kinds of interpretations in the proof assistant Isabelle/HOL. We report on our integration of matrix interpretations, arctic interpretations, and nonlinear polynomial interpretations over various domains, including the reals.

 

  PDF |    doi:10.1007/978-3-319-08918-8_30  |  © Springer International Publishing Switzerland

BibTeX 

@inproceedings{CSRT-RTATLCA14,
author = "Christian Sternagel and Ren{\'e} Thiemann",
title = "Formalizing Monotone Algebras for Certification of
Termination and Complexity Proofs",
booktitle = "Proceedings of the Joint 25th International Conference on
Rewriting Techniques and Applications and 12th
International Conference on Typed Lambda Calculi and Applications",
series = "Lecture Notes in Computer Science (Advanced Research in
Computing and Software Science)",
editor = "Gilles Dowek",
volume = 8560,
pages = "441--455",
year = 2014,
doi = "10.1007/978-3-319-08587-6_13",
}
Nach oben scrollen