A General Type for Storage Operators

TL;DR

This paper extends the type system AF2 to provide a more general typing for storage operators in lambda calculus, facilitating the simulation of call-by-value within call-by-name contexts.

Contribution

It introduces a generalized type for storage operators in an extended AF2 system and suggests potential extensions to other type systems.

Findings

A new general type for storage operators in an extended AF2 system.

A proposed generalization to other type systems without detailed proof.

Enhanced understanding of typing for storage operators in lambda calculus.

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.