Abstract:
Thirty-five years ago, thunks were used to simulate
call-by-name under call-by-value in Algol 60. Twenty years ago, Plotkin
presented continuation-based simulations of call-by-name under call-by-value
and vice versa in the -calculus. We connect all three of these
classical simulations by factorizing the continuation-based call-by-name
simulation with a thunk-based call-by-name simulation
followed by the continuation-based call-by-value simulation
extended to thunks. We show that actually satisfies all of
Plotkin's correctness criteria for (i.e., his Indifference,
Simulation, and Translation theorems). Furthermore, most of the correctness
theorems for can now be seen as simple corollaries of the
corresponding theorems for and .
Available as PostScript, PDF,
DVI.
|