How to translate the axiom schema of induction by Curry-Howard?
First a correction. The statement
$$\forall P \,.\, (P(0) \Rightarrow (\forall n . P(n) \Rightarrow P(S n)) \Rightarrow \forall m . P(m)),$$
is not the schema of induction, but rather induction written in second-order arithmetic.
To get the schema you need to avoid $\forall P$. This is done by saying that there are infinitely many axioms of the form
$$P(0) \Rightarrow (\forall n . P(n) \Rightarrow P(S n)) \Rightarrow \forall m . P(m),$$
one for each formula $P(x)$. That is, whereas in your axiom $P$ refers to arbitrary subsets of $\mathbb{N}$, in the schema it refers to sytnactic entities, namely formulas with parameter $x$. It is called a "schema" because it prescribes a shape from which infinitely many axioms may be generated by plugging in all possible syntactic entities $P$.

To answer your question, we just have to look at the Curry-Howard correspondence to see what a predicate $P(x)$ correspond to. The answer is type family or dependent type. Because you wrote your axiom in second-order arithmetic, it became unclear how to quantify over dependent types. This is possible by using universes, for instance Daimano in his answer used $\mathsf{Prop}$, the universe of propositions. However, under the pure Curry-Howard there is no $\mathsf{Prop}$, there are only types.

We have two options. If we translate the schema, then it is this: for every dependent type $$x : \mathbb{N} \vdash P(x) \, \mathsf{type}$$ we get the type
$$\textstyle P(0) \to (\prod_{n:\mathbb{N}} P(n) \to P(S n)) \to \prod_{m:\mathbb{N}} P(m)$$
If we translate the second-order formulation of induction, we need to use a type universe $\mathsf{Type}$, and then we get
$$\textstyle 
\prod_{P : \mathbb{N} \to \mathsf{Type}}
P(0) \to (\prod_{n:\mathbb{N}} P(n) \to P(S n)) \to \prod_{m:\mathbb{N}} P(m)$$

What are these types inhabited by? In the case of schema, they are inhabited by primitive recursors $\mathsf{rec}_P$ which satisfy the equations
\begin{align*}
\mathsf{rec}_P \; z \; f \; 0 &amp;= z \\
\mathsf{rec}_P \; z \; f \; (S n) &amp;= f \; n \; (\mathsf{rec}_P \; z \; f \; n)
\end{align*}
Depending on the details of your formalism we may be able to drop the subscript $P$ on $\mathsf{rec}_P$, and just write $\mathsf{rec}$ -- but secretly there is a different $\mathsf{rec}$ for each $P$.

In the case of the second-order induction we would get a single primitive recursor $\mathsf{rec}$ satisfying
\begin{align*}
\mathsf{rec} \; P \; z \; f \; 0 &amp;= z \\
\mathsf{rec} \; P \; z \; f \; (S n) &amp;= f \; n \; (\mathsf{rec} \;P \; z \; f \; n)
\end{align*}

If I spoke to a Haskell programmer I would say that in the case of schema each $\mathsf{rec}$ was obtained from $P$ using a "deriving" clause, whereas in the second-order case there is a single polymorphic $\mathsf{rec}$.