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 π-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 π-calculus. Plotkin completes the picture by showing that there is a convergent correspondence from the λ-calculus into SECD.