How to translate the axiom schema of induction by Curry-Howard? I'm trying to understand the Curry-Howard correspondence. I am comfortable with it for propositional logic, but get confused when $\forall, \exists$ quantifiers come in the picture.

The axiom schema of induction (in second-order logic) is  $\forall P. \left[(P(0) \implies \forall k\in \mathbb N. (P(k)\implies P(k+1)))\implies \forall n\in \mathbb N. P(n)\right]$.

To my understanding, via Curry-Howard every statement gets translated to a type. Proving a statement means showing that the type is inhabited. For example, +, = are dependent types taking two parameters of type nat; every $\forall k\in A$ gets translated into a dependent product $\prod_{k::A}$. So the axiom schema should become something like 
$
\left[\prod_{P::?} \left((P\, 0) \rightarrow \left(\prod_{k::\mathbb N} (P \, k)\rightarrow P \, (+\, k\, 1) \right)\right)\right]\rightarrow \prod_{n::\mathbb N}(P \,n)
$

A difficulty arises when translating $\forall P$: what is the type of $P$? The problem is that, in order for the above to make sense, $(P\, k)$ is supposed to be a type for all $k::\mathbb N$ (so we are allowed to say $(P\, 0) \rightarrow \cdots$, for instance). So $P$ seems to me like a (dependent) type constructor taking a nat as parameter. But then we are taking a product over $P$, so we must be able to treat $P$ as an element of a type! The problem seems to boil down to, are type constructors themselves of some type? Can we write this statement without having to refer to such a type? Perhaps higher-order logic translates to higher-order type theory, but I do not know the latter. References would also be appreciated.
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}$.