Proof and computational complexity I couldn't find documents elaborating on this: if the Curry Howard correspondence is to be interpreted as establishing a strong relation between proofs and programs, should there not be a strong relation between proof and computational complexity?
I'm asking this as a reference request.
Maybe the keyword you are looking for is &quot;Implicit Complexity&quot;. It is more general than Curry-Howard correspondence, but several lines of research investigate along the axis you are interested in. You can check for instance the publications of Patrick Baillot for many references and pointers.
For a little self-promotion, here are for instance two recent papers [KPP1,KPP2] characterizing via the Curry-Howard correspondence on certain cyclic proofs the following complexity classes, depending on the logical rules incorporated or not in the cyclic proof system:

Regular languages (no contraction, no cut) [KPP1]
DLogSpace (contraction, no cut) [KPP1]
Primitive recursive functions (cut, no contraction) [KPP2]
Gödel's System T (cut, contraction) [KPP2]

[KPP1] Cyclic Proofs and Jumping Automata. Kuperberg, Pinault, Pous, FSTTCS 2019
[KPP2] Cyclic Proofs, System T and the power of Contraction. Kuperberg, Pinault, Pous, POPL 2021