Thunks and the λ-calculus

John Hatcliff, Olivier Danvy

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review


    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 [script C]n with a thunk-based call-by-name simulation [script T] followed by the continuation-based call-by-value simulation [script C]v, extended to thunks.

    formula here

    We show that [script T] actually satisfies all of Plotkin's correctness criteria for [script C]n (i.e. his Indifference, Simulation and Translation theorems). Furthermore, most of the correctness theorems for [script C]n can now be seen as simple corollaries of the corresponding theorems for [script C]v and [script T].
    Original languageEnglish
    JournalJournal of Functional Programming
    Pages (from-to)303-319
    Number of pages17
    Publication statusPublished - 1997


    Dive into the research topics of 'Thunks and the λ-calculus'. Together they form a unique fingerprint.

    Cite this