Verifying Termination and Reduction Properties about Higher-Order Logic Programs

We describe two checkers for verifying termination and reduction properties about higher-order logic programs. The reduction checker verifies that the result of a program execution is structurally smaller than (or equal to) the inputs to the program. The termination checker guarantees that the inputs of the recursive calls are structurally smaller than the inputs of the original call, taking into account reduction properties. At the heart of both checkers lies an inference system to reason about structural properties, which are described by higher-order subterm relations. This approach provides a logical foundation for proving properties such as termination and reduction and factors the effort required for each one of them. Moreover, it allows the study of proof-theoretical properties, soundness, and completeness and different optimizations. The termination and reduction checker are implemented as part of the Twelf system and have been used on a wide variety of examples, including proofs about typed assembly language and those in the area of proof-carrying code.