A general storage theorem for integers in call-by-name \(\lambda\)- calculus (Q1329740)

The result presented here is part of a general program which aims at proving that all features of imperative programming can be efficiently simulated within (lazy) call-by-name \(\lambda\)-calculus. The notion of ``storage operators'' has been introduced by the author in order to simulate the call-by-value strategy and to modelize assignment instructions. The main result about storage operators is that there is a simple second- order type for them, using Gödel's not-not-translation. Krivine gives here a new and simpler proof of a stronger version of this theorem, which contains in particular his previous results concerning the typing of storage operators in intuitionistic and in classical logic. This striking result, whose proof remains technically involved, gives rise to new storage theorems, and can be given a rather intuitive meaning in terms of realisability.