From light logics to type assignments: a case study

TY - JOUR

T1 - From light logics to type assignments

T2 - a case study

AU - Gaboardi, Marco

AU - Rocca, Simona Ronchi Della

PY - 2009/10

Y1 - 2009/10

N2 - Using Soft Linear Logic (SLL) as case study, we analyze a method for transforming a light logic into a type assignment system for the ?-calculus, inheriting the complexity properties of the logics. Namely the typing assures the strong normalization in a number of steps polynomial in the size of the term, and moreover all polynomial functions can be computed by ?-terms that can be typed in the system. The proposed method is general enough to be used also for other light logics.

AB - Using Soft Linear Logic (SLL) as case study, we analyze a method for transforming a light logic into a type assignment system for the ?-calculus, inheriting the complexity properties of the logics. Namely the typing assures the strong normalization in a number of steps polynomial in the size of the term, and moreover all polynomial functions can be computed by ?-terms that can be typed in the system. The proposed method is general enough to be used also for other light logics.

U2 - 10.1093/jigpal/jzp019

DO - 10.1093/jigpal/jzp019

M3 - Article

SN - 1367-0751

VL - 17

SP - 499

EP - 530

JO - Logic Journal of the Interest Group in Pure and Applied Logic (IGPL) (Logic Journal of the IGPL)

JF - Logic Journal of the Interest Group in Pure and Applied Logic (IGPL) (Logic Journal of the IGPL)

IS - 5

ER -