Characterizing polynomial and exponential complexity classes in elementary lambda-calculus.

In this paper an implicit characterization of the complexity classes k - EXP and k - FEXP , for k ≥ 0 , is given, by a type assignment system for a stratified λ -calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic ( ELL ), and the hierarchy of complexity classes k - EXP is characterized by a hierarchy of types. [ABSTRACT FROM AUTHOR]