A reflection on call-by-value

Amr Sabry, Philip Wadler

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

One way to model a sound and complete translation from a source calculus into a target calculus is with an adjoint or a Galois connection. In the special case of a reflection, one also has that the target calculus is isomorphic to a subset of the source. We show that three widely studied translations form reflections. We use as our source language Moggi's computational lambda calculus, which is an extension of Plotkin's call-by-value calculus. We show that Plotkin's CPS translation, Moggi's monad translation, and Girard's translation to linear logic can all be regarded as reflections form this source language, and we put forward the computational lambda calculus as a model of call-by-value computation that improves on the traditional call-by-value calculus. Our work strengthens Plotkin's and Moggi's original results and improves on recent work based on equational correspondence, which uses equations rather than reductions.
Original languageEnglish
Pages (from-to)916-941
Number of pages26
JournalACM Letters on Programming Languages and Systems
Issue number6
Publication statusPublished - 1 Nov 1997


Dive into the research topics of 'A reflection on call-by-value'. Together they form a unique fingerprint.

Cite this