The most comprehensive survey of the relationship between constructive proof theory (which is tied closely to the theory of constructive ordinals) and second-order impredicative arithmetic (which as Ulrik points out is equivalent in strength to System F) is Girard (1989). There he builds on his theory of dilators (1981), which I don't really follow, but I think essentially provides a nonconstructive theory of higher-order Skolemisation.
My understanding is that you can't express $\Sigma^1_2$ formulae constructively in the Bishop—Martin-Löf sense, because they are impredicative in a way you can't eliminate by adding any sort of first-order induction scheme.
I remember suggesting to an ordinal theorist that one could simply stipulate that you can ground an impredicative constructivism in a type theory based on the polymorphic lambda calculus, and use the reduction candidate technique from Girard's SN proof for System F to impose a reasonable total order on the universe of constructions, calling the equivalence classes you get from this the ordinals; he said something intelligent which I took away as saying you might get that to work, but it would have all the advantages of theft over honest toil. To get it to work, it is not good enough that you can prove in set theory the existence of such ordinals, you would need a constructive proof of trichotomy for the order.
To sum up, with the regular notion of intuitionistic construction due to Bishop—Martin-Löf, the literature I know of strongly suggests no. If you are averse to honest toil and would embrace an impredicative constructivism, then my guess is that it can probably be done. You would, naturally, need a stronger theory that System F to constructively prove the required trichotomy, but the Calculus of Inductive Constructions provides an obvious candidate.
- Girard, Jean-Yves (1981), $\Pi^1_2$-logic. I. Dilators, Annals of Mathematical Logic 21 (2): 75–219.
- Girard (1989) Proof Theory and Logical Complexity, vol. I, Napoli: Bibliopolis. There is no volume II.