Lambda and pi calculi, CAM and SECD machines

Abstract

We analyse machines that implement the call-by-value reduction strategy of the λ-calculus: two environment machines – CAM and SECD – and two encodings into the $\pi$ -calculus – due to Milner and Vasconcelos. To establish the relation between the various machines, we setup a notion of reduction machine and two notions of correspondences: operational – in which a reduction step in the source machine is mimicked by a sequence of steps in the target machine – and convergent – where only reduction to normal form is simulated. We show that there are operational correspondences from the λ-calculus into CAM, and from CAM and from SECD into the $\pi$ -calculus. Plotkin completes the picture by showing that there is a convergent correspondence from the λ-calculus into SECD.