TY - JOUR

T1 - Call-by-name, Call-by-value, Call-by-need, and the Linear Lambda Calculus

AU - Maraist, John

AU - Odersky, Martin

AU - Turner, David N.

AU - Wadler, Philip

N1 - MFPS XI, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference

PY - 1995

Y1 - 1995

N2 - Girard described two translations of intuitionistic logic into linear logic, one where A -> B maps to (!A) -o B, and another where it maps to !(A -o B). We detail the action of these translations on terms, and show that the first corresponds to a call-by-name calculus, while the second corresponds to call-by-value. We further show that if the target of the translation is taken to be an affine calculus, where ! controls contraction but weakening is allowed everywhere, then the second translation corresponds to a call-by-need calculus, as recently defined by Ariola, Felleisen, Maraist, Odersky and Wadler. Thus the different calling mechanisms can be explained in terms of logical translations, bringing them into the scope of the Curry-Howard isomorphism.

AB - Girard described two translations of intuitionistic logic into linear logic, one where A -> B maps to (!A) -o B, and another where it maps to !(A -o B). We detail the action of these translations on terms, and show that the first corresponds to a call-by-name calculus, while the second corresponds to call-by-value. We further show that if the target of the translation is taken to be an affine calculus, where ! controls contraction but weakening is allowed everywhere, then the second translation corresponds to a call-by-need calculus, as recently defined by Ariola, Felleisen, Maraist, Odersky and Wadler. Thus the different calling mechanisms can be explained in terms of logical translations, bringing them into the scope of the Curry-Howard isomorphism.

U2 - 10.1016/S1571-0661(04)00022-2

DO - 10.1016/S1571-0661(04)00022-2

M3 - Article

SN - 1571-0661

VL - 1

SP - 370

EP - 392

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -