存储操作员和系统TTR的所有正类型
Storage operators and forall-positive types of system TTR
摘要：
1990年，J.L. Krivine引入了存储操作符的概念来模拟“按名称调用”策略中的“按值调用”。J.L. Krivine已经证明，使用经典逻辑到直觉逻辑的哥德尔翻译，我们可以在AF 2型系统中找到存储算子的简单类型。本文研究了TTR型系统的$\forall$ -正型（全称二阶量词在这些正型中出现）和Gödel变换（经典Gödel变换的推广）。我们利用句法方法推广了J.L. Krivine定理关于这些类型和这些变换。我们在递归整数类型的情况下证明了这个结果。
英文摘要：
In 1990, J.L. Krivine introduced the notion of storage operator to simulate "call by value" in the "call by name" strategy. J.L. Krivine has shown that, using Gödel translation of classical into intuitionitic logic, we can find a simple type for the storage operators in AF2 type system. This paper studies the $\forall$-positive types (the universal second order quantifier appears positively in these types), and the Gödel transformations (a generalization of classical Gödel translation) of TTR type system. We generalize, by using syntaxical methods, the J.L. Krivine's Theorem about these types and for these transformations. We give a proof of this result in the case of the type of recursive integers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
