I&C Journal 2018 Journal Article
Characterizing polynomial and exponential complexity classes in elementary lambda-calculus
- Patrick Baillot
- Erika De Benedetti
- Simona Ronchi Della Rocca
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.