@inproceedings{1fe37464ba2a43179a879f1e07c069df,

title = "A soft type assignment system for λ-calculus",

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 ?-calculus (STA), which assigns to ?-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 subject reduction and normalization, and it is correct and complete for PTIME and PTIME.",

keywords = "LAMBDA-CALCULUS, POLYNOMIAL-TIME, LINEAR LOGIC",

author = "Marco Gaboardi and {Della Rocca}, {Simona Ronchi}",

year = "2007",

doi = "10.1007/978-3-540-74915-8_21",

language = "English",

isbn = "9783540749141",

series = "Lecture notes in computer science",

publisher = "Springer ",

pages = "253--267",

editor = "Jacques Duparc and Henzinger, {Thomas A.}",

booktitle = "Computer Science Logic",

note = "21st International Workshop on Computer Science Logic, CSL 2007/16th Annual Conference of the EACSL ; Conference date: 11-09-2007 Through 15-09-2007",

}