Gradual Session Types

Atsushi Igarashi; Peter Thiemann; Vasco Vasconcelos; Philip Wadler

doi:10.1145/3110282

Gradual Session Types

Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, Philip Wadler

Research output: Contribution to journal › Article › peer-review

Abstract / Description of output

Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing.
We propose Gradual GV as an extension of the functional session type system GV with dynamic types and casts. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types
requires a novel approach to specifying the dynamics of the language.

Original language	English
Article number	38
Pages (from-to)	1-28
Number of pages	28
Journal	Proceedings of the ACM on Programming Languages
Volume	1
Issue number	IFCP
DOIs	https://doi.org/10.1145/3110282
Publication status	Published - 29 Aug 2017

Access to Document

10.1145/3110282Licence: Creative Commons: Attribution (CC-BY)

icfp17-main76Final published version, 359 KBLicence: Creative Commons: Attribution (CC-BY)

http://dl.acm.org/citation.cfm?doid=3136534.3110282Licence: Creative Commons: Attribution (CC-BY)

From Data Types to Session Types - A Basis for Concurrency and Distribution
Wadler, P.
EPSRC
20/05/13 → 19/11/20
Project: Research

Philip Wadler, FRS
- wadlerinf.ed.acuk
- School of Informatics - Chair of Theoretical Computer Science
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active

Cite this

@article{1bbbaa98b3004fe8bd92c84171fe87dc,

title = "Gradual Session Types",

abstract = "Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose Gradual GV as an extension of the functional session type system GV with dynamic types and casts. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic typesrequires a novel approach to specifying the dynamics of the language. ",

author = "Atsushi Igarashi and Peter Thiemann and Vasco Vasconcelos and Philip Wadler",

year = "2017",

month = aug,

day = "29",

doi = "10.1145/3110282",

language = "English",

volume = "1",

pages = "1--28",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery (ACM)",

number = "IFCP",

}

TY - JOUR

T1 - Gradual Session Types

AU - Igarashi, Atsushi

AU - Thiemann, Peter

AU - Vasconcelos, Vasco

AU - Wadler, Philip

PY - 2017/8/29

Y1 - 2017/8/29

N2 - Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose Gradual GV as an extension of the functional session type system GV with dynamic types and casts. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic typesrequires a novel approach to specifying the dynamics of the language.

AB - Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose Gradual GV as an extension of the functional session type system GV with dynamic types and casts. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic typesrequires a novel approach to specifying the dynamics of the language.

U2 - 10.1145/3110282

DO - 10.1145/3110282

M3 - Article

SN - 2475-1421

VL - 1

SP - 1

EP - 28

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - IFCP

M1 - 38

ER -

Gradual Session Types

Abstract / Description of output

Access to Document

Fingerprint

Projects

From Data Types to Session Types - A Basis for Concurrency and Distribution

Profiles

Philip Wadler, FRS

Cite this