Proving Program Termination in Higher Order Logic

We suggest two simple additions to packages that use wellfounded recursion to justify termination of recursive programs: * The contraction condition, to be proved in cases when termination conditions are difficult or impossible to extract automatically; * user-supplied inductive invariants in cases of nested recursion. We have implemented these additions in Isabelle/HOL and demonstrated their usefulness on a large example of the recursive BDD algorithm Apply. The paper uses a simple predicate on functionals in higher order logic as an approximate model of program termination. We explore this model and prove that for every functional there exists a largest ``domain of termination''''.