Paper Info
Title
A semantical storage operator theorem for all types
Abstract
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.
Year
DOI
Venue
1998
10.1016/S0168-0072(97)00041-9
Annals of Pure and Applied Logic
Keywords
Field
DocType
λ-calculus,Types,AF2 type system,Storage operators,Gödel translations
Discrete mathematics,Algebra,Gödel,Pure mathematics,Operator (computer programming),Mathematics
Journal
Volume
Issue
ISSN
91
1
0168-0072
Citations 
PageRank 
References 
1
0.39
7
Authors
1
Name
Order
Citations
PageRank
Christophe Raffalli1295.55