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

John Maraist, Martin Odersky, David Turner, Philip Wadler

Technical Report #5/95, Fakultaet fuer Informatik, University of Karlsruhe

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.