Gradual session types. (2019)
- Record Type:
- Journal Article
- Title:
- Gradual session types. (2019)
- Main Title:
- Gradual session types
- Authors:
- IGARASHI, ATSUSHI
THIEMANN, PETER
TSUDA, YUYA
VASCONCELOS, VASCO T.
WADLER, PHILIP - Abstract:
- 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 a gradually typed extension of the functional session type system GV. Following a standard framework of gradual typing, Gradual GV consists of an external language, which relaxes the type system of GV using dynamic types; an internal language with casts, for which operational semantics is given; and a cast-insertion translation from the former to the latter. 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.
- Is Part Of:
- Journal of functional programming. Volume 29(2019)
- Journal:
- Journal of functional programming
- Issue:
- Volume 29(2019)
- Issue Display:
- Volume 29, Issue 2019 (2019)
- Year:
- 2019
- Volume:
- 29
- Issue:
- 2019
- Issue Sort Value:
- 2019-0029-2019-0000
- Page Start:
- Page End:
- Publication Date:
- 2019
- Subjects:
- Functional programming (Computer science) -- Periodicals
- Journal URLs:
- http://journals.cambridge.org/action/displayJournal?jid=JFP ↗
http://firstsearch.oclc.org ↗ - DOI:
- 10.1017/S0956796819000169 ↗
- Languages:
- English
- ISSNs:
- 0956-7968
- Deposit Type:
- Legaldeposit
- View Content:
- Available online (eLD content is only available in our Reading Rooms) ↗
- Physical Locations:
- British Library STI - ELD Digital store
- Ingest File:
- 12117.xml