Functions as Session-Typed Processes

Bernardo Toninho; Luís Manuel Marques da Costa Caires; Frank Pfenning

doi:10.1007/978-3-642-28729-9_23

Functions as Session-Typed Processes

Bernardo Toninho, Luís Manuel Marques da Costa Caires, Frank Pfenning

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

33 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 language	Unknown
Title of host publication	Lecture Notes in Computer Science
Pages	346-360
DOIs	https://doi.org/10.1007/978-3-642-28729-9_23
Publication status	Published - 1 Jan 2012
Event	FoSSaCS 2012 - 15th International Conference on Foundations of Software Science and Computation Structures - Duration: 1 Jan 2012 → …

Conference

Conference	FoSSaCS 2012 - 15th International Conference on Foundations of Software Science and Computation Structures
Period	1/01/12 → …

Access to Document

10.1007/978-3-642-28729-9_23

Cite this

@inproceedings{d2105a93911248fea3457132fef719a5,

title = "Functions as Session-Typed Processes",

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.",

author = "Bernardo Toninho and Caires, {Lu{\'i}s Manuel Marques da Costa} and Frank Pfenning",

year = "2012",

month = jan,

day = "1",

doi = "10.1007/978-3-642-28729-9_23",

language = "Unknown",

isbn = "978-3-642-28728-2",

pages = "346--360",

booktitle = "Lecture Notes in Computer Science",

note = "FoSSaCS 2012 - 15th International Conference on Foundations of Software Science and Computation Structures ; Conference date: 01-01-2012",

}

TY - GEN

T1 - Functions as Session-Typed Processes

AU - Toninho, Bernardo

AU - Caires, Luís Manuel Marques da Costa

AU - Pfenning, Frank

PY - 2012/1/1

Y1 - 2012/1/1

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-28729-9_23

DO - 10.1007/978-3-642-28729-9_23

M3 - Conference contribution

SN - 978-3-642-28728-2

SP - 346

EP - 360

BT - Lecture Notes in Computer Science

T2 - FoSSaCS 2012 - 15th International Conference on Foundations of Software Science and Computation Structures

Y2 - 1 January 2012

ER -