CPS transforms have long been important tools in the study of programming languages, especially those related to the λ-calculus. Recently, it has been shown that encodings into process calculi, such as the π-calculus, can also serve as semantics, in the same way as CPS transforms. It is known that common encodings of the call-by-value and call-by-name λ-calculi into the π-calculus can be seen as CPS transforms composed with a naming transform that expresses sharing of values.

We review this analysis and extend it to call-by-need. The new call-by-need CPS transform requires extending the target λ-calculus with an effect, which we call constructive update. We present a proof of the correctness of the call-by-need CPS transform, which is hence a new proof of the correctness of the call-by-need π-calculus encoding. Also, we derive abstract machines from the CPS transforms discussed.