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.
|Number of pages||32|
|Journal||Logic Journal of the Interest Group in Pure and Applied Logic (IGPL) (Logic Journal of the IGPL)|
|Publication status||Published - Oct 2009|