Evaluating functions as processes

Beniamino Accattoli
(Carnegie Mellon University)

A famous result by Milner is that the lambda-calculus can be simulated inside the pi-calculus. This simulation, however, holds only modulo strong bisimilarity on processes, i.e. there is a slight mismatch between beta-reduction and how it is simulated in the pi-calculus. The idea is that evaluating a lambda-term in the pi-calculus is like running an environment-based abstract machine, rather than applying ordinary beta-reduction. In this paper we show that such an abstract-machine evaluation corresponds to linear weak head reduction, a strategy arising from the representation of lambda-terms as linear logic proof nets, and that the relation between the two is as tight as it can be. The study is also smoothly rephrased in the call-by-value case, introducing a call-by-value analogous of linear weak head reduction.

In Rachid Echahed and Detlef Plump: Proceedings 7th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2013), Rome, 23th March 2013, Electronic Proceedings in Theoretical Computer Science 110, pp. 41–55.
Published: 25th February 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.110.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org