id: 01067875
dt: j
an: 01067875
au: Hatcliff, John; Danvy, Olivier
ti: Thunks and the $λ$-calculus.
so: J. Funct. Program. 7, No.3, 303-319 (1997).
py: 1997
pu: Cambridge University Press, Cambridge
la: EN
cc: 
ut: thunks; $λ$-calculus
ci: 
li: doi:10.1017/S0956796897002748
ab: Summary: 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 ${\cal C}_n$ with a thunk-based call-by-name
    simulation $\cal T$ followed by the continuation-based call-by-value
    simulation ${\cal C}_v$ extended to thunks. $$\matrixΛ& @> {\cal T}>>&
    Λ_{\text{thunks}}\ \underset{{\cal C}_n}\to{\searrow} && @VV{\cal C}_v
    V\ && Λ_{\text{CPS}}\endmatrix$$ We show that ${\cal T}$ actually
    satisfies all of Plotkin’s correctness criteria for ${\cal C}_n$
    (i.e. his Indifference, Simulation and Translation theorems).
    Furthermore, most of the correctness theorems for ${\cal C}_n$ can now
    be seen as simple corollaries of the corresponding theorems for ${\cal
    C}_v$ and ${\cal T}$.
rv: