Formalizing monotone algebras for certification of termination- and complexity proofs

ABSTRACT. Monotone algebras are frequently utilized 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. Here, we report on our integration of matrix interpretations, arctic interpretations, and non-linear polynomial interpretations over various domains, including the reals.