Gradual Session Types

Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, Philip Wadler

Research output: Contribution to journalArticlepeer-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 languageEnglish
Article number38
Pages (from-to)1-28
Number of pages28
JournalProceedings of the ACM on Programming Languages
Issue numberIFCP
Publication statusPublished - 29 Aug 2017


Dive into the research topics of 'Gradual Session Types'. Together they form a unique fingerprint.

Cite this