Logic Journal of IGPL Advance Access published online on July 4, 2009
Logic Journal of IGPL, doi:10.1093/jigpal/jzp019
| ||||||||||||||||||||||||||||||||||||||||||||||||||
From Light Logics to Type Assignments: a case study
Dipartimento di Informatica, Università degli Studi di Torino. Corso Svizzera 185, 10149 Torino, Italy. E-mail: gaboardi{at}di.unito.it
Dipartimento di Informatica, Universitàa degli Studi di Torino. Corso Svizzera 185, 10149 Torino, Italy. E-mail: ronchi{at}di.unito.it
| Abstract |
|---|
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.
Key Words: type assignment implicit computational complexity lambda calculus polynomial time
Received for publication 11 May 2009.
![]()
CiteULike
Connotea
Del.icio.us What's this?