Soft Linear Logic (SLL) is a subsystem of second-order linear logic with restricted rules for exponentials, which is correct and complete for PTIME. We design a type assignment system for the lambda-calculus (STA), which assigns to lambda-terms as types (a proper subset of ) SLL formulas, in such a way that typable terms inherit the good complexity properties of the logical system. Namely STA enjoys sub ject reduction and normalization, and it is correct and complete for PTIME and FPTIME.
A Soft Type Assignment System for Lambda-Calculus
GABOARDI, MARCO GIUSEPPE;RONCHI DELLA ROCCA, Simonetta
2007-01-01
Abstract
Soft Linear Logic (SLL) is a subsystem of second-order linear logic with restricted rules for exponentials, which is correct and complete for PTIME. We design a type assignment system for the lambda-calculus (STA), which assigns to lambda-terms as types (a proper subset of ) SLL formulas, in such a way that typable terms inherit the good complexity properties of the logical system. Namely STA enjoys sub ject reduction and normalization, and it is correct and complete for PTIME and FPTIME.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
