A Reflection on Call-by-Value.pdf

A Re ection on Call-by-ValueAMR SABRYUniversity of OregonandPHILIP WADLERBell Laboratories, Lucent TechnologiesOne way to model a sound and complete translation from a source calculus into a target calculusis with an adjoint or a Galois connection. In the special case of a re ection, one also has that thetarget calculus is isomorphic to a subset of the source. We show that three widely studied trans-lations form re ections. We use as our source language Moggis computational lambda calculus,which is an extension of Plotkins call-by-value calculus. We show that Plotkins CPS transla-tion, Moggis monad translation, and Girards translation to linear logic can all be regarded asre ections from this source language, and we put forward the computational lambda calculus asa model of call-by-value computation that improves on the traditional call-by-value calculus. Ourwork strengthens Plotkins and Moggis original results and improves on recent work based onequational correspondence, which uses equations rather than reductions.Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Applicative (Func-tional) Programming; D.3.4 [Programming Languages]: Processors|compilers; F.3.2 [Logicsand Meanings of Programs]: Semantics of Programming Languages; F.4.1 [MathematicalLogic and Formal Languages]: Mathematical LogicGeneral Terms: Languages, TheoryAdditional Key Words and Phrases: Category theory, compiling, continuations, Galois connections1. INTRODUCTIONCompiler correctness is a central concern of computing. It is often expressed in theform of a diagram. MM NN#-T -S? 6#This article is a revised and extended version of a paper that appeared in the ACM SIGPLANInternational Conference on Functional Programming (Philadelphia, Pa.), 1996. Work startedwhile the rst author was at Chalmers University, and the second author was at University ofGlasgow.Authors addresses: A. Sabry, University of Oregon, Department of Computer and InformationScience, Eugene, OR 97403; P. Wadle