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

Angaben zum Objekt

• Standort: Deutsche Nationalbibliothek Frankfurt am Main
• Umfang: Online-Ressource
• Sprache: Englisch
• Anmerkungen: Journal of functional programming. - 29 (2019) , e17, ISSN: 1469-7653

Beteiligte, Orts- und Zeitangaben

• Ereignis: Veröffentlichung
• (wo): Freiburg
• (wer): Universität
• (wann): 2021
• Urheber: Thiemann, Peter ; Tsuda, Yuya ; Igarashi, Atsushi ; Vasconcelos, Vasco ; Wadler, Philip
• Beteiligte Personen und Organisationen: Albert-Ludwigs-Universität Freiburg. Programmiersprachen

Weitere Informationen

• DOI: 10.1017/S0956796819000169
• URN: urn:nbn:de:bsz:25-freidok-2193366
• Rechteinformation: Der Zugriff auf das Objekt ist unbeschränkt möglich.
• Letzte Aktualisierung: 25.03.2025, 13:44 MEZ