Is there any work relating type systems and Cook-Reckhow proof systems? An important subfield of computational complexity is proof complexity, mostly due to Cook and Reckhow. E.g. one notable result is that a proof system that has efficient proofs (i.e., in length polynomial to the formula being proven) for all tautologies could be constructed iff $coNP$ = $NP$. Other results deal with specific propositional calculus proof systems, showing that they all have superpolynomial proof lower-bounds. Is there any work relating type systems and type inference rules to the proof systems as defined in this theory? 

In general, a cursory examination reveals that most discussions of type systems discuss computability (decidability/undecidability) with little discussion of finer complexity bounds (which may well exist in many finite models). Is there a reason why this is so (if indeed it is so)?
Cook-Reckhow propositional proof systems are nonunifrom.
E.g. the computational complexity counterpart to
the class of polynomial-size $\mathsf{Extended Frege}$ proofs is 
the nonuniform complexity class $\mathsf{P/poly}$.
We have to look at their uniform counterparts: 
E.g. the proof complexity counterpart for $\mathsf{P}$ are 
bounded arithmetic theories like
Cook's theory $\mathsf{PV}$ (standing for polynomial-time verifiable),
Buss's theory $\mathsf{S}^1_2$, ...

Cook and Urquhart used Cook's theory $\mathsf{PV}$ 
to define a theory of higher-types polynomial-time computable functions $\mathsf{PV}^\omega$ in the following paper:


Stephen A. Cook and Alasdair Urquhart, "Functional interpretations of feasibly constructive arithmetic", 1993. doi: 10.1016/0168-0072(93)90044-E


There has been some follow up work which you can find by looking at articles citing this paper. 

Implicit complexity theory that Martin mentions is also influenced by this work. Check out Simone Martini's survey slides and Ugo Dal Lago's survey article to get a picture of what is implicit complexity theory and its history.