A REFLECTION ON CALL-BY-VALUE

A number of compilers exploit the following strategy: translate a term to continuation-passing style (CPS) and optimize the resulting term u sing a sequence of reductions. Recent work suggests that an alternativ e strategy is superior: optimize directly in an extended source calcul us. We suggest that the appropriate relation between the source and ta rget calculi may be captured by a special case of a Galois connection known as a reflection. Previous work has focused on the weaker notion of an equational correspondence, which is based on equality rather tha n reduction. We show that Moggi's monad translation and Plotkin's CPS translation can both be regarded as reflections, and thereby strengthe n a number of results in the literature.