We study type-directed encodings of the simply-typed λ-calculus in a session-typed π-calculus. The translations proceed in two steps: standard embeddings of simply-typed λ-calculus in a linear λ-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 π-calculus processes subject to a session type discipline. We show that the resulting translations induce sharing and copying parallel evaluation strategies for the original λ-terms, thereby providing a new logically motivated explanation for these strategies. © 2012 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Toninho, B., Caires, L., & Pfenning, F. (2012). Functions as session-typed processes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7213 LNCS, pp. 346–360). https://doi.org/10.1007/978-3-642-28729-9_23
Mendeley helps you to discover research relevant for your work.