Gradual session types
Abstract: Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services 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 GradualGV 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
- Location
-
Deutsche Nationalbibliothek Frankfurt am Main
- Extent
-
Online-Ressource
- Language
-
Englisch
- Notes
-
Proceedings of the ACM on programming languages. - 1, ICFP (2017) , 38, ISSN: 2475-1421
- Event
-
Veröffentlichung
- (where)
-
Freiburg
- (who)
-
Universität
- (when)
-
2021
- Creator
- Contributor
- DOI
-
10.1145/3110282
- URN
-
urn:nbn:de:bsz:25-freidok-2193414
- Rights
-
Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Last update
-
14.08.2025, 10:43 AM CEST
Data provider
Deutsche Nationalbibliothek. If you have any questions about the object, please contact the data provider.
Associated
- Igarashi, Atsushi
- Thiemann, Peter
- Vasconcelos, Vasco
- Wadler, Philip
- Albert-Ludwigs-Universität Freiburg. Programmiersprachen
- Universität
Time of origin
- 2021
Other Objects (12)
Gradual session types
LJGS: Gradual security types for object-oriented languages
Artifact for "Gradual Session Types", appearing in ACM SIGPLAN International Conference on Functional Programming
Artifact for "Gradual Session Types", appearing in ACM SIGPLAN International Conference on Functional Programming
Label-dependent session types
Relating functional and imperative session types
Gradual security typing
Duality of session types: the final cut
Polymorphic lambda calculus with context-free session types
Label dependent lambda calculus and gradual typing
Designing libraries : LAG poster session
Nested Session Types
Gradual session types
LJGS: Gradual security types for object-oriented languages
Artifact for "Gradual Session Types", appearing in ACM SIGPLAN International Conference on Functional Programming
Artifact for "Gradual Session Types", appearing in ACM SIGPLAN International Conference on Functional Programming
Label-dependent session types
Relating functional and imperative session types
Gradual security typing
Duality of session types: the final cut
Polymorphic lambda calculus with context-free session types
Label dependent lambda calculus and gradual typing
Designing libraries : LAG poster session
Nested Session Types
Gradual session types
LJGS: Gradual security types for object-oriented languages
Artifact for "Gradual Session Types", appearing in ACM SIGPLAN International Conference on Functional Programming
Artifact for "Gradual Session Types", appearing in ACM SIGPLAN International Conference on Functional Programming
Label-dependent session types
Relating functional and imperative session types
Gradual security typing
Duality of session types: the final cut
Polymorphic lambda calculus with context-free session types
Label dependent lambda calculus and gradual typing
Designing libraries : LAG poster session