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.
M. Cimini, C. Sacerdoti Coen, D. Sangiorgi (2010). Functions as Processes: Termination and the lambda mu mu~ - Calculus. BERLIN : Springer.
Functions as Processes: Termination and the lambda mu mu~ - Calculus
SACERDOTI COEN, CLAUDIO;SANGIORGI, DAVIDE
2010
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
