Type theory and computational complexity Is there a type system, which restricts the lambda terms to the terms which fall inside a complexity class? Like the typable terms in the theory are strictly inside the complexity class ? Or is it not possible at all?

I find the there are lot of studies on expressibility of the type theory, like provably terminating, extended polynomials etc.. But is there any way to restrict that to a complexity class?
The keywords you are looking for are "Implicit Computational Complexity". The field studies for instance variants of linear logic and the complexity bounds they can guarantee on the terms underlying the derivations.