Paper Info
Title
Lazy Evaluation and Delimited Control
Abstract
The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics. By a series of reasoning steps, we systematically unpack the standard-order reduction relation of the calculus and discover a novel abstract machine definition which, like the calculus, goes "under lambdas." We prove that machine evaluation is equivalent to standard-order evaluation. Unlike traditional abstract machines, delimited control plays a significant role in the machine's behavior. In particular, the machine replaces the manipulation of a heap using store-based effects with disciplined management of the evaluation stack using control-based effects. In short, state is replaced with control. To further articulate this observation, we present a simulation of call-by-need in a call-by-value language using delimited control operations.
Year
DOI
Venue
2010
10.2168/LMCS-6(3:1)2010
LOGICAL METHODS IN COMPUTER SCIENCE
Keywords
DocType
Volume
call-by-need,reduction semantics,abstract machines,delimited continuations,lambda calculus
Journal
6
Issue
ISSN
Citations 
3
1860-5974
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Ronald Garcia113913.53
Andrew Lumsdaine22754236.74
Amr Sabry352035.46