Functions as Session-Typed Processes

<p>We study type-directed encodings of the simply-typed <em>λ</em>-calculus in a session-typed <em>π</em>-calculus. The translations proceed in two steps: standard embeddings of simply-typed <em>λ</em>-calculus in a linear <em>λ</em>-calculus, followed by a standard translation of linear natural deduction to linear sequent calculus. We have shown in prior work how to give a Curry-Howard interpretation of the proofs in the linear sequent calculus as <em>π</em>-calculus processes subject to a session type discipline. We show that the resulting translations induce sharing and copying parallel evaluation strategies for the original <em>λ</em>-terms, thereby providing a new logically motivated explanation for these strategies.</p>