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?