Size-based termination of higher-order rewrite systems. F. Blanqui. Submitted, 57 pages, 2015.

Several authors devised termination criteria for fixpoint-based function definitions in λ-calculi with inductively defined types, using deduction rules for bounding the size of a term defined as its rank in the inductive type. In the present paper, we extend this approach to rewriting-based function definitions and more general notion of sizes.