A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types

Abstract

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. © 2009 Springer Berlin Heidelberg.