I am looking for references about efficient type theories, efficiency in the sense of computational complexity, and type theory in the sense of Martin-Lof's type theories. Has there been any studies with the goal of creating efficient versions of these theories?
Note: I am familiar with Stephen Cook and Alasdair Urquhart's theory $\mathsf{PV^\omega}$ and their "Functional Interpretations of Feasibly Constructive Arithmetic" paper from 1989 (doi:10.1145/73007.73017), but that is type theory in the sense of Kurt Godel's System $\mathsf{T}$. I am looking for feasible type theories in the sense of Martin-Lof's type theory.