Abstract

Using Soft Linear Logic 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