λ-calculus as such is not a computational model. A reduction strategy is needed. In this paper, we consider λ-calculus with the left reduction. This strategy has many advantages: it always terminates when applied to a normalizable λ-term and it seems more economic since we compute λ-term only when we need it. But the major drawback of this strategy is that a function must compute its argument every time it uses it. This is the reason why this strategy is not really used. In 1990 Krivine (1990b) introduced the notion of storage operators in order to avoid this problem and to simulate call-by-value when necessary. The AF2 type system is a way of interpreting the proof rules for second-order intuitionistic logic plus equational reasoning as construction rules for terms. Krivine (1990b) has shown that, by using Gödel translation from classical to intuitionistic logic (denoted byg), we can find in system AF2 a very simple type for storage operators. Historically the type was discovered before the notion of storage operator itself. Krivine (1990a) proved that as far as totality of functions is concerned second-order classical logic is conservative over second-order intuitionistic logic. To prove this, Krivine introduced the following notions: A[x] is an input (resp. output) data type if one can prove intuitionistically A[x] → Ag[x] (resp. Ag[x] → ⇁⇁A[x]). Then if A[x] is an input data type and B[x] is an output data type, then if one can prove A[x] → B[x] classically one can prove it intuitionistically. The notion of storage operator was discovered by investigating the property of all λ-terms of type Ng[x] → ⇁⇁N[x] where N[x] is the type of integers. Parigot (1992) and Krivine (1994) have extended the AF2 system to classical logic. The method of Krivine is very simple: it consists of adding a new constant, denoted by C, with the declaration С: ∀X{⇁⇁ X → X} which axiomatizes classical logic over intuitionistic logic. For the constant C, he adds a new reduction rule which is a particular case of a rule given by Felleisen (1987) for control operator.