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)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history
Request removal from index
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 28,829
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
On the Logic of Β -Pregroups.Aleksandra Kiślak-Malinowska - 2007 - Studia Logica 87 (2-3):323 - 342.
Compact Bracket Abstraction in Combinatory Logic.Sabine Broda & Luís Damas - 1997 - Journal of Symbolic Logic 62 (3):729-740.
The Abstract Variable-Binding Calculus.Don Pigozzi & Antonino Salibra - 1995 - Studia Logica 55 (1):129 - 179.
-Calculus and Böhm's Theorem.René David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
Variable Binding Term Operators in $\Lambda $-Calculus.M. W. Bunder - 1979 - Notre Dame Journal of Formal Logic 20 (4):876-878.
Topological Representation of the Lambda-Calculus.Steve Awodey - 2000 - Mathematical Structures in Computer Science 10 (1):81-96.

Monthly downloads

Added to index


Total downloads

40 ( #130,908 of 2,178,184 )

Recent downloads (6 months)

1 ( #316,497 of 2,178,184 )

How can I increase my downloads?

My notes
Sign in to use this feature

There  are no threads in this forum
Nothing in this forum yet.

Other forums