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.

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.
Lecture Notes in Computer Science
73
86
M. Cimini; C. Sacerdoti Coen; D. Sangiorgi
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11585/100214
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 2
social impact