Alexander Krauss:

Certified Size-Change Termination

We develop a formalization of the Size-Change Principle in Isabelle/HOL and use it to construct formally certified termination proofs for recursive functions automatically.

PDF document

The formal Isabelle theories described in this paper are now part of the Isabelle/HOL Library. They can be found in the directory HOL/SizeChange of the Isabelle Distribution.