Nour, Karim Proper storage operators. (Opérateurs propres de mise en mémoire.) (French. Abridged English version) Zbl 0788.03015 C. R. Acad. Sci., Paris, Sér. I 317, No. 1, 1-6 (1993). Summary: Storage operators were introduced by J.-L. Krivine [Arch. Math. Log. 30, 241-267 (1990; Zbl 0712.03009)]; they are closed \(\lambda\)-terms which, for some fixed data type (for example integers), allow to simulate call by value while using call by name. J.-L. Krivine showed such operators can be typed, in the type system \({\mathcal A} {\mathcal F}2\), using Gödel’s translation from classical to intuitionistic logic. In this note we study the problem of typing those storage operators which give a closed term as result (we call them proper storage operators). We give restrictive conditions on the type system \({\mathcal A} {\mathcal F}2\) so as to obtain proper operators. This study will be restricted to the case of Church integers. Cited in 1 Document MSC: 03B40 Combinatory logic and lambda calculus 68Q65 Abstract data types; algebraic specification Keywords:closed \(\lambda\)-terms; call by value; call by name; type system; typing; storage operators; closed term; Church integers Citations:Zbl 0712.03009 PDFBibTeX XMLCite \textit{K. Nour}, C. R. Acad. Sci., Paris, Sér. I 317, No. 1, 1--6 (1993; Zbl 0788.03015)