Is there any work relating type systems and Cook-Reckhow proof systems?
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.