Type theory and computational complexity
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.