A Soft Type Assignment System for Lambda-Calculus

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.