Inductive Invariants for Nested Recursion
TPHOLs, pp. 253-269, 2003.
input outputhigher order logic
We show that certain input-output relations, termed induc- tive invariants are of central importance for termination proofs of al- gorithms dened by nested recursion. Inductive invariants can be used to enhance recursive function denition packages in higher-order logic mechanizations. We demonstrate the usefulness of inductive invariants ...More
Full Text (Upload PDF)
PPT (Upload PPT)