Higer-Order Linear Ramified Recurrence

Higher-Order Linear Ramified Recurrence (HOLRR) is a linear (affine) lambda-calculus - every variable occurs at most once - extended with a recursive scheme on free algebras. One simple condition on type derivations enforces both polytime completeness and a strong notion of polytime soundness on typeable terms. Completeness for poly-time holds by embedding Leivant's ramified recurrence on words into HOLRR. Soundness is established at all types - and not only for first order terms. Type connectives are limited to tensor and linear implication. Moreover, typing rules are given as a simple deductive system