Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs?

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,...

Full description

Bibliographic Details
Main Authors: Christian Sternagel, Rene ́ Thiemann
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Subjects:
Arctic
Online Access:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.657.1888
http://www.jaist.ac.jp/%7Ec-sterna/publications/Sternagel-Thiemann-RTA-TLCA14.pdf
id ftciteseerx:oai:CiteSeerX.psu:10.1.1.657.1888
record_format openpolar
spelling ftciteseerx:oai:CiteSeerX.psu:10.1.1.657.1888 2023-05-15T14:54:39+02:00 Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs? Christian Sternagel Rene ́ Thiemann The Pennsylvania State University CiteSeerX Archives application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.657.1888 http://www.jaist.ac.jp/%7Ec-sterna/publications/Sternagel-Thiemann-RTA-TLCA14.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.657.1888 http://www.jaist.ac.jp/%7Ec-sterna/publications/Sternagel-Thiemann-RTA-TLCA14.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.jaist.ac.jp/%7Ec-sterna/publications/Sternagel-Thiemann-RTA-TLCA14.pdf text ftciteseerx 2016-01-08T16:40:02Z 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 inter-pretations over various domains, including the reals. 1 Text Arctic Unknown Arctic
institution Open Polar
collection Unknown
op_collection_id ftciteseerx
language English
description 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 inter-pretations over various domains, including the reals. 1
author2 The Pennsylvania State University CiteSeerX Archives
format Text
author Christian Sternagel
Rene ́ Thiemann
spellingShingle Christian Sternagel
Rene ́ Thiemann
Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs?
author_facet Christian Sternagel
Rene ́ Thiemann
author_sort Christian Sternagel
title Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs?
title_short Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs?
title_full Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs?
title_fullStr Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs?
title_full_unstemmed Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs?
title_sort formalizing monotone algebras for certification of termination and complexity proofs?
url http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.657.1888
http://www.jaist.ac.jp/%7Ec-sterna/publications/Sternagel-Thiemann-RTA-TLCA14.pdf
geographic Arctic
geographic_facet Arctic
genre Arctic
genre_facet Arctic
op_source http://www.jaist.ac.jp/%7Ec-sterna/publications/Sternagel-Thiemann-RTA-TLCA14.pdf
op_relation http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.657.1888
http://www.jaist.ac.jp/%7Ec-sterna/publications/Sternagel-Thiemann-RTA-TLCA14.pdf
op_rights Metadata may be used without restrictions as long as the oai identifier remains attached to it.
_version_ 1766326418772328448

Similar Items