Loading...
Please wait, while we are loading the content...
Similar Documents
Call-by-Name, Call-by-Value, Call-by-Need, and the Linear Lambda Calculus (1995)
| Content Provider | CiteSeerX |
|---|---|
| Author | Wadler, Philip Odersky, Martin Turner, David N. Maraist, John |
| Abstract | Girard described two translations of intuitionistic logic into linear logic, one where A ! B maps to (!A) \Gammaffi B, and another where it maps to !(A \Gammaffi B). We detail the action of these translations on terms, and show that the first corresponds to a callby -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. 1 Introduction Plotkin, in "Call-by-name, call-by-value and the -calculus" [25], demonstrated how two different calling mechanisms could be explained by two different translations into continuation passing style. At the tim... |
| File Format | |
| Publisher Date | 1995-01-01 |
| Access Restriction | Open |
| Subject Keyword | Second Translation Corresponds Control Contraction Curry-howard Isomorphism Linear Lambda Calculus Continuation Passing Style Introduction Plotkin Second Corresponds Different Translation Affine Calculus Call-by-need Calculus Callby Name Calculus Logical Translation |
| Content Type | Text |
