  There are two possible computational interpretations of second-order
arithmetic: Girard's system F or Spector's bar recursion and its variants.
While the logic is the same, the programs obtained from these two
interpretations have a fundamentally different computational behavior and their
relationship is not well understood. We make a step towards a comparison by
defining the first translation of system F into a simply-typed total language
with a variant of bar recursion. This translation relies on a realizability
interpretation of second-order arithmetic. Due to G\"odel's incompleteness
theorem there is no proof of termination of system F within second-order
arithmetic. However, for each individual term of system F there is a proof in
second-order arithmetic that it terminates, with its realizability
interpretation providing a bound on the number of reduction steps to reach a
normal form. Using this bound, we compute the normal form through primitive
recursion. Moreover, since the normalization proof of system F proceeds by
induction on typing derivations, the translation is compositional. The
flexibility of our method opens the possibility of getting a more direct
translation that will provide an alternative approach to the study of
polymorphism, namely through bar recursion.
