Let me add to the above (perfectly correct) answers that there is a more general perspective, which works for all positive connectives, of which sums are a special case.
The fundamental insight is that reducibility actually arises from a duality between terms and contexts, which is itself parametric in a set of terms closed under certain operations (such as $\beta$-expansion, but I think something trickier must be used for strong normalization), called a pole. Given a pole $P$, one defines
$$\mathsf C\perp t\quad\text{just if}\quad\mathsf C[t]\in P$$
where $\mathsf C$ is a context (a term with a hole denoted by $\bullet$) and $t$ a term. The idea is that $P$ is a set of terms which "behave well" (e.g. they have a normal form), so $\mathsf C\perp t$ means that the context $\mathsf C$ and the term $t$ "interact well" with respect to the property expressed by $P$.
Given a set $S$ of contexts, one may define a set of terms
$$S^\bot:=\{t\mathrm{|}\forall\mathsf C\in S,\,\mathsf C\perp t\}.$$
A similar definition induces a set of contexts from a set of terms $T$, which we still denote by $T^\bot$.
We may then define the interpretation of a type $A$, which is a set of contexts denoted by $|A|$, by induction on $A$:
$$
\begin{array}{rcl}
|X| &:=& \{\bullet\} \\
|A\to B| &:=& \{\mathsf C[\bullet\,u]\mathrel{|} u\in|A|^\bot,\ \mathsf C\in|B|\} \\
|A\times B| &:=& \{\mathsf C[\pi_1\bullet]\mathrel{|}\mathsf C\in|A|\}\cup\{\mathsf C[\pi_2\bullet]\mathrel{|}\mathsf C\in|B|\}\\
|A+B| &:=& \{\mathsf C\mathrel{|}\mathsf C[\mathsf{inl}\,\bullet]\in |A|^{\bot\bot}\text{ and }\mathsf C[\mathsf{inr}\,\bullet]\in|B|^{\bot\bot}\}
\end{array}
$$
Finally, we let
$$\|A\|:=|A|^\bot,$$
which is a set of terms. This is the "reducibility predicate" on $A$.
One then goes on to prove the so-called adequacy theorem: if
$$x_1:C_1,\ldots,x_n:C_n\vdash t:A$$
is derivable, then for all $u_1,\ldots,u_n$, $u_i\in\|C_i\|$ implies $t[u_1/x_1,\ldots,u_n/x_n]\in\|A\|$. This is proved by induction on the last rule of the derivation, using the properties of the pole (closure under $\beta$-expansion or something like that).
Now, if things are setup correctly, one also has $x\in\|A\|$ as well as $\|A\|\subseteq P$ for every variable $x$ and every type $A$, which implies that every term belongs to the pole by adequacy, i.e., every term "behaves well".
I am sure that this works for weak normalization, i.e., one may take $P$ to be the set of weakly normalizing terms (which is closed under $\beta$-expansion) and immediately obtain weak normalization of the simply-typed $\lambda$-calculus with sums. For strong normalization, some kind of hack is needed, because $\beta$-expanding a strongly normalizable term does not necessarily yield a strongly normalizable term, but I'm sure that a suitable definition will make things work.
This "reducibility by duality" may be found already in Girard's Linear logic paper (1987), although I'm not sure he is the one who introduced it. It has been used by many authors since then and of course it easily extends to higher order quantification. In particular, the above presentation is adapted from Krivine, who uses it as the basis of his classical realizablity theory (see his many papers on the subject, all available on his web page).
