To appear in: CONCUR'09

Abstract

A logical interpretation of the λ-calculus into the π-calculus, preserving spine reduction and types.
by S. van Bakel and M.G. Vigliotti

To appear in proceedings of CONCUR'09.

We define a new, output-based encoding of the λ-calculus into the asynchronous π-calculus, enriched with pairing, that has its origin in mathematical logic, and show that this encoding respects one-step spine-reduction up to substitution, and that normal substitution is respected up to similarity. We will also show that it fully encodes lazy reduction of closed terms, in that term-substitution as well as each reduction step are modelled up to similarity. We then define a notion of type assignment for the π-calculus that uses the type constructor →, and show that all Curry-assignable types are preserved by the encoding.

@Inproceedings{Bakel-Vigliotti-CONCUR'09, Author = {S. van Bakel and M.G. Vigliotti}, Title = {{A logical interpretation of the $`l$-calculus into the $`p$-calculus, preserving spine reduction and types}}, Booktitle = {Proceedings of 20th International Conference on Concurrency Theory (CONCUR'09), {\rm Bologna, Italy} Editor = {M. Bravetti and G. Zavattaro}, Series = lncs, Volume = {5710}, Publisher = {Springer-Verlag}, Pages = {84 -- 98}, Year = {2009} }