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. (shrink)

We introduce a new type system called “System ST” , based on subtyping, and prove the basic property of the system. We show the extraordinary expressive power of the system which leads us to think that it could be a good candidate for doing both proof and extraction of programs.