English

A General Type for Storage Operators

Logic 2009-05-06 v1

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.

Cite

@article{arxiv.0905.0549,
  title  = {A General Type for Storage Operators},
  author = {Karim Nour},
  journal= {arXiv preprint arXiv:0905.0549},
  year   = {2009}
}
R2 v1 2026-06-21T12:58:14.197Z