A semantical storage operator theorem for all types (Q1382182)

The notion of storage operator was introduced by J.-L. Krivine to simulate, for a given set of terms, ``call by value'' in a ``call by name''. The storage operator theorem is valid for a type \(D\) if any term of type \(\neg D\to\neg D^*\) is a storage operator for the elements of \(D\) (\(D^*\) being the Gödel translation of \(D\)). Krivine proved the storage operator theorem for the type of integer in the AF2 type system. This result has been extended to any type with only positive \(\forall\)-quantifiers by Krivine, using a semantical proof, and by Nour (using a syntactic proof). The author gives a new notion of semantical storage operator which is equivalent to Krivine and Nour's notion for data-types. Its new storage operator theorem gives a sufficient condition to ensure the existence of semantical storage operators for an arbitrary type. The proof technique is a simplification of Krivine's techniques using only 2 variables (while Nour uses the directed \(\lambda\)-calculus).