Storage operators and directed lambda-calculus

Journal of Symbolic Logic 60 (4):1054-1086 (1995)
Storage operators have been introduced by J. L. Krivine in [5] they are closed λ-terms which, for a data type, allow one to simulate a "call by value" while using the "call by name" strategy. In this paper, we introduce the directed λ-calculus and show that it has the usual properties of the ordinary λ-calculus. With this calculus we get an equivalent--and simple--definition of the storage operators that allows to show some of their properties: $\bullet$ the stability of the set of storage operators under the β-equivalence (Theorem 5.1.1); $\bullet$ the undecidability (and semidecidability) of the problem "is a closed λ-term t a storage operator for a finite set of closed normal λ-terms?" (Theorems 5.2.2 and 5.2.3); $\bullet$ the existence of storage operators for every finite set of closed normal λ-terms (Theorem 5.4.3); $\bullet$ the computation time of the "storage operation" (Theorem 5.5.2)
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2275874
 Save to my reading list
Follow the author(s)
Edit this record
My bibliography
Export citation
Find it on Scholar
Mark as duplicate
Request removal from index
Revision history
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 31,396
Through your library
References found in this work BETA
Opérateurs de Mise En Mémoire Et Traduction de Gödel.Jean-Louis Krivine - 1990 - Archive for Mathematical Logic 30 (4):241-267.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles
Topological Representation of the Lambda-Calculus.Steve Awodey - 2000 - Mathematical Structures in Computer Science 10 (1):81-96.
Variable Binding Term Operators in $\Lambda $-Calculus.M. W. Bunder - 1979 - Notre Dame Journal of Formal Logic 20 (4):876-878.
-Calculus and Böhm's Theorem.René David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
The Abstract Variable-Binding Calculus.Don Pigozzi & Antonino Salibra - 1995 - Studia Logica 55 (1):129 - 179.
Compact Bracket Abstraction in Combinatory Logic.Sabine Broda & Luís Damas - 1997 - Journal of Symbolic Logic 62 (3):729-740.
On the Logic of Β -Pregroups.Aleksandra Kiślak-Malinowska - 2007 - Studia Logica 87 (2-3):323 - 342.
Added to PP index

Total downloads
44 ( #132,243 of 2,225,996 )

Recent downloads (6 months)
4 ( #141,474 of 2,225,996 )

How can I increase my downloads?

Monthly downloads
My notes
Sign in to use this feature