U. Dal Lago, S. Martini, and L. Roversi
Higher-order linear ramified
recurrence
In Proceedings of TYPES'04, volume 3085 of LNCS, pages
178 - 193 Springer-Verlag, December 2004
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 |
.ps.gz ]
Back
This file has been generated by
bibtex2html 1.43