×

Proper storage operators. (Opérateurs propres de mise en mémoire.) (French. Abridged English version) Zbl 0788.03015

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.

MSC:

03B40 Combinatory logic and lambda calculus
68Q65 Abstract data types; algebraic specification

Citations:

Zbl 0712.03009
PDFBibTeX XMLCite