Functions as Session-Typed Processes

Research output: Chapter in Book/Report/Conference proceedingConference contribution

21 Citations (Scopus)

Abstract

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.
Original languageUnknown
Title of host publicationLecture Notes in Computer Science
Pages346-360
DOIs
Publication statusPublished - 1 Jan 2012
EventFoSSaCS 2012 - 15th International Conference on Foundations of Software Science and Computation Structures -
Duration: 1 Jan 2012 → …

Conference

ConferenceFoSSaCS 2012 - 15th International Conference on Foundations of Software Science and Computation Structures
Period1/01/12 → …

Cite this