A General Type for Storage Operators
Karim Nour · Mathematical logic quarterly · 1995
Abstract In 1990, J. L. Krivine introduced the notion of storage operator to simulate, in λ‐calculus, the “call by value” in a context of a “call by name”. J. L. Krivine has showed that, using Gödel translation from classical to intuitionistic logic, we can find a simple type for storage operators in AF2 type system. In the present paper we give a general type for storage operators in a slight extension of AF2. At the end we give (without proof) a generalization of this result to other types.