Inductive Invariants for Nested Recursion

TPHOLs, pp. 253-269, 2003.

Cited by: 11|Bibtex|Views2|Links
EI
Keywords:
input outputhigher order logic

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments