| Abstract |
| 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 |
@inproceedings{DalLago+Martini+Roversi:2004-TYPES,
volume = {3085},
author = {Dal Lago, Ugo and Martini, Simone and Roversi, Luca},
series = {Lecture Notes in Computer Science},
booktitle = {Proceedings of TYPES'03},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2004-TYPES/DalLagoMartiniRoversi2004TYPES.ps.gz},
title = {Higer-Order Linear Ramified Recurrence},
abstract = {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},
copyrightspringer = {http://www.springer.de/comp/lncs/index.html},
publisher = {Springer Verlag},
pages = {178--193},
year = {2004},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
