Session types for rust

Thomas Bracht Laumann Jespersen; Philip Munksgaard; Ken Friis Larsen

doi:10.1145/2808098.2808100

Session types for rust

Thomas Bracht Laumann Jespersen, Philip Munksgaard, Ken Friis Larsen

Department of Computer Science

25 Citations (Scopus)

Abstract

We present a library for specifying session types implemented in Rust, and discuss practical use cases through examples and demonstrate how session types may be used in a large-scale application. Specifically we adapt parts of the ad-hoc communication patterns in the Servo browser engine to use session typed channels. Session types provide a protocol abstraction, expanding on traditional typed communication channels, to ensure that communication takes place according to a specified protocol. Thus, the library allows us to provide compile-time guarantees of adherence to a specific protocol without incurring significant run-time penalties.

Original language	English
Title of host publication	Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming : WGP 2015
Number of pages	10
Publisher	Association for Computing Machinery
Publication date	30 Aug 2015
Pages	13-22
ISBN (Print)	978-1-4503-3810-3
DOIs	https://doi.org/10.1145/2808098.2808100
Publication status	Published - 30 Aug 2015
Event	ACM SIGPLAN Workshop on Generic Programming 2015 - Vancouver, British Columbia, Canada Duration: 31 Aug 2015 → 2 Sept 2015 Conference number: 11

Conference

Conference	ACM SIGPLAN Workshop on Generic Programming 2015
Number	11
Country/Territory	Canada
City	Vancouver, British Columbia
Period	31/08/2015 → 02/09/2015

Access to Document

10.1145/2808098.2808100

Cite this

@inbook{b8947c22fc7548249795ee8a801790cb,

title = "Session types for rust",

abstract = "We present a library for specifying session types implemented in Rust, and discuss practical use cases through examples and demonstrate how session types may be used in a large-scale application. Specifically we adapt parts of the ad-hoc communication patterns in the Servo browser engine to use session typed channels. Session types provide a protocol abstraction, expanding on traditional typed communication channels, to ensure that communication takes place according to a specified protocol. Thus, the library allows us to provide compile-time guarantees of adherence to a specific protocol without incurring significant run-time penalties.",

keywords = "Rust, Session types, concurrency, generic types",

author = "Jespersen, {Thomas Bracht Laumann} and Philip Munksgaard and Larsen, {Ken Friis}",

year = "2015",

month = aug,

day = "30",

doi = "10.1145/2808098.2808100",

language = "English",

isbn = "978-1-4503-3810-3",

pages = "13--22",

booktitle = "Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming",

publisher = "Association for Computing Machinery",

note = "ACM SIGPLAN Workshop on Generic Programming 2015, ICFP 2015 ; Conference date: 31-08-2015 Through 02-09-2015",

}

TY - CHAP

T1 - Session types for rust

AU - Jespersen, Thomas Bracht Laumann

AU - Munksgaard, Philip

AU - Larsen, Ken Friis

N1 - Conference code: 11

PY - 2015/8/30

Y1 - 2015/8/30

N2 - We present a library for specifying session types implemented in Rust, and discuss practical use cases through examples and demonstrate how session types may be used in a large-scale application. Specifically we adapt parts of the ad-hoc communication patterns in the Servo browser engine to use session typed channels. Session types provide a protocol abstraction, expanding on traditional typed communication channels, to ensure that communication takes place according to a specified protocol. Thus, the library allows us to provide compile-time guarantees of adherence to a specific protocol without incurring significant run-time penalties.

AB - We present a library for specifying session types implemented in Rust, and discuss practical use cases through examples and demonstrate how session types may be used in a large-scale application. Specifically we adapt parts of the ad-hoc communication patterns in the Servo browser engine to use session typed channels. Session types provide a protocol abstraction, expanding on traditional typed communication channels, to ensure that communication takes place according to a specified protocol. Thus, the library allows us to provide compile-time guarantees of adherence to a specific protocol without incurring significant run-time penalties.

KW - Rust, Session types, concurrency, generic types

U2 - 10.1145/2808098.2808100

DO - 10.1145/2808098.2808100

M3 - Book chapter

SN - 978-1-4503-3810-3

SP - 13

EP - 22

BT - Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming

PB - Association for Computing Machinery

T2 - ACM SIGPLAN Workshop on Generic Programming 2015

Y2 - 31 August 2015 through 2 September 2015

ER -

Session types for rust

Abstract

Conference

Access to Document

Fingerprint

Cite this