Ugo Dal Lago, Simone Martini, and Luca Roversi. Higher order linear ramified recurrence. In Types Conference, Post-Workshop Proceedings, Lecture Notes in Computer Science. Springer, 2004. To appear.

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 typable 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

[ bib | http ]

Back