Call-by-name, call-by-value, call-by-need and the linear lambda calculus

J. Maraist, M. Odersky, D.N. Turner, P. Wadler

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Girard described two translations of intuitionistic logic into linear logic, one where A→B maps to (!A⊸B) and another where it maps to !(A⊸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. Our results extend neatly to translations of extensions for recursion in the call-by-name and call-by-value calculi, and in general to extensions for products and for the corresponding untyped systems.

Original languageEnglish
Pages (from-to)175-210
Number of pages36
JournalTheoretical Computer Science
Volume228
Issue number1-2
DOIs
Publication statusPublished - Oct 1999

Fingerprint

Dive into the research topics of 'Call-by-name, call-by-value, call-by-need and the linear lambda calculus'. Together they form a unique fingerprint.

Cite this