Storage Operators and ∀-positive Types in TTR Type System

摘要: In 1990, J. L. Krivine introduced the notion of storage operator to simulate “call by value” in name” strategy. has showed that, using Godel translation classical into intuitionistic logic, one can find a simple type for operators AF2 system. This paper studies ∀-positive types (the universal second order quantifier appears positively these types) and transformations (a generalization translation) TTR We generalize syntactical methods Krivine's theorem about transformations. give proof this result case recursive integers. Mathematics Subject Classification: 03B40, 68Q60.