A General Type for Storage Operators
classification
🧮 math.LO
keywords
storagetypeoperatorscallgeneralgivekrivinecalculus
read the original abstract
In 1990, J.L. Krivine introduced the notion of storage operator to simulate, in $\lambda$-calculus, the "call by value" in a context of a "call by name". J.L. Krivine has shown that, using G\"odel translation from classical into intuitionistic logic, we can find a simple type for storage operators in AF2 type system. In this present paper, we give a general type for storage operators in a slight extension of AF2. We give at the end (without proof) a generalization of this result to other types.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.