Automatic Certification of Termination Proofs


We present our Isabelle/HOL formalization of rewriting and the resulting,
fully automatic, certifier for termination proofs. We start at the basic
library design and proceed by highlighting some of the supported
techniques: the dependency pair transformation, the subterm criterion, and
root-labeling. The last technique depends on the termination preservation
of signature extensions, for which we give the first mechanized proof.