一句话：首次将 System F 翻译到带 bar recursion 的简单类型全语言，并基于可实现性给出归一化解释。
System F 与 Spector 的 bar recursion 可分别计算解释二阶算术，但所得程序的计算行为迥异，二者关系尚不清楚。本文定义首个从 System F 到带 bar recursion 变体的简单类型全语言的翻译。翻译依赖二阶算术的可实现性解释：虽然由 Gödel 不完备定理无法在二阶算术内证明 System F 整体终止，但对每个 System F 项，二阶算术可证明其终止，且可实现性解释给出到达范式所需归约步数的界。作者利用该界通过原始递归计算范式；由于 System F 的归一化证明按类型推导归纳进行，翻译是组合式的。该工作为通过 bar recursion 研究多态性提供了新途径。
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ödel'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.