A reflection on call-by-value

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 …