My graduate student Harley Eades and I have recently completed a draft paper on normalization for a type theory called Stratified System F (SSF), using the idea of hereditary substitution.  SSF was originally studied by Daniel Leivant and then Leivant and Norman Danner.  See papers like “Finitely Stratified Polymorphism” (sorry, subscription link), or “Stratified Polymorphism and Primitive Recursion”, for example.  SSF is like System F, except that every type is kinded at a certain level (just a natural number).  So universal types look like $\forall X:*_p. T$, where $p$ is a natural number.  The universal quantification itself has a level higher than $p$ and than the level of the body $T$ (this is a minor change from Leivant’s system, where the quantification just has to have level greater than $p$)).  The critical restriction is that when you instantiate a universal type, you must do so at a level at or below the level $p$ declared for the variable.  This greatly restricts the complexity of the functions one can write: indeed, the set of functions representable in SSF is much smaller than the set of primitive recursive functions, which in turn is much, much smaller than the set representable in System F.