Higer-Order Linear Ramified Recurrence

DAL LAGO, U.; Martini,; Roversi, Luca

doi:10.1007/b98246

CINECA IRIS Institutional Research Information System

IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Torino.

AperTO è l'archivio istituzionale Open Access destinato a raccogliere, rendere visibile e conservare la produzione scientifica dell'Università degli Studi di Torino.

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

Titolo:	Higer-Order Linear Ramified Recurrence
Autori Riconosciuti:	U. DAL LAGO MARTINI ROVERSI, Luca mostra contributor esterni nascondi contributor esterni
Autori:	U. DAL LAGO; MARTINI; L. ROVERSI
Data di pubblicazione:	2004
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 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
Volume:	3085/2004
Pagina iniziale:	178
Pagina finale:	193
Nome del convegno:	TYPES'04
Luogo del convegno:	Jouy-en-Josas (FRANCE)
Anno del convegno:	December 2004
Digital Object Identifier (DOI):	10.1007/b98246
URL:	http://www.di.unito.it/~rover/
Rivista:	LECTURE NOTES IN COMPUTER SCIENCE
Appare nelle tipologie:	04B-Conference paper in rivista

File in questo prodotto:

File	Descrizione	Tipologia	Licenza
DalLagoMartiniRoversiTYPES2004.pdf		1 Ver. finale autore	Accesso riservato	Utenti riconosciuti Richiedi una copia

Utilizza questo identificativo per citare o creare un link a questo documento:
http://hdl.handle.net/2318/23065

Citazioni

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.