What is the precise connection between:
strong normalization of the simply typed $\lambda$-calculus, and
cut elimination for (intuitionistic) propositional logic (limited to implication) in “sequent calculus” form?
Does either follow from the other? Does each follow from the other? (Do they have the same computational complexity and/or arithmetic strength?)
I can vaguely see that, under the Curry-Howard correspondence, a redex $(\lambda (v:\sigma).E)T$ will translate to a natural deduction style proof with $\rightarrow$ introduction immediately followed by $\rightarrow$ elimination, which becomes a cut proof in sequent calculus, whose immediate elimination should correspond to the reduct $E[v := T]$. So certainly there should be some connection. The precise details escape me, however, in particular because terms in the s.t.$\lambda$.c. correspond to natural deduction proofs whereas cut elimination takes place at the sequent calculus level (there are three things in correspondence: a $\lambda$-term, a natural deduction proof and a sequent calculus proof, and I'm not sure what the correct statement at the “natural deduction” level should be that corresponds to the two bullet points at the “$\lambda$-calculs” and “sequent calculus” levels).
I'm sure this is very standard: is there a textbook that explains this, hopefully in a pleasant way?