constant, denoted by $C$, with the declaration $C : \q X \{ \neg \neg X \f X \}$ which axiomatizes classical logic over intuitionistic logic. For the constant $C$, he adds a new reduction rule : $(C t t_1 ... t_n) \f (t \quad \l x (x \quad t_1 ... t_n))$ which is a particular case of a rule given by Felleisen for control operator (see \[1\]). In this system the property of the unicity of integers representation is lost, but J-L. Krivine has shown that storage operators typable in the intuitionistic system $AF2$ can be used to find the values of classical integers [^1](see \[6\]).\
The latter result suggests also many questions :

-   What is the relation between classical integers and the type $N$\*$[x]$ ?

-   Why do we need intuitionistic logic to modelize the assignment instruction and classical logic to modelize the control operators ?

In this paper, we present a new classical type system based on a logical system called mixed logic. This system allows essentially to distinguish between classical proofs and intuitionistic proofs. We prove that, in this system, we can characterize, by types, the storage operators and the control operators. This results give some 