A semantical storage operator theorem for all types Original Research Article

Storage operators are λ-terms which simulate call-by-value in call-by-name for a given set of terms. Krivineʹs storage operator theorem shows that any term of type ¬D → ¬D∗, where D∗ is the Gödel translation of D, is a storage operator for the terms of type D when D is a data-type or a formula with only positive second order quantifiers. We prove that a new semantical version of Krivineʹs theorem is valid for every types. This also gives a simpler proof of Krivineʹs theorem using the properties of data-types.