Functions as Processes: Termination and the lambda mu mu~ - Calculus

The the lambda mu mu~ - calculus is a variant of the lambda-calculus with significant differences, including non-confluence and a Curry-Howard isomorphism with the classical sequent calculus. We present an encoding of the lambda mu mu~ - calculus into the pi-calculus. We establish the operational correctness of the encoding, and then we extract from it an abstract machine for the former calculus. We prove that there is a tight relationship between such a machine and Curien and Herbelin's abstract machine. The pi-calculus image of the (typed) lambda mu mu~ - calculus is a nontrivial set of terminating processes