Nested session types
From MaRDI portal
Publication:2233456
Abstract: Session types statically describe communication protocols between concurrent message-passing processes. Unfortunately, parametric polymorphism even in its restricted prenex form is not fully understood in the context of session types. In this paper, we present the metatheory of session types extended with prenex polymorphism and, as a result, nested recursive datatypes. Remarkably, we prove that type equality is decidable by exhibiting a reduction to trace equivalence of deterministic first-order grammars. Recognizing the high theoretical complexity of the latter, we also propose a novel type equality algorithm and prove its soundness. We observe that the algorithm is surprisingly efficient and, despite its incompleteness, sufficient for all our examples. We have implemented our ideas by extending the Rast programming language with nested session types. We conclude with several examples illustrating the expressivity of our enhanced type system.
Recommendations
Cites work
- \(L(A)=L(B)\)? A simplified decidability proof.
- A generalization of the trie data structure
- A principled approach to programming with nested types in Haskell
- Behavioral polymorphism and parametricity in session-based communication
- Bisimilarity on basic process algebra is in 2-ExpTime (an explicit proof)
- Bounded polymorphism in session types
- Context-free session types
- Decidability of DPDA equivalence
- Deciding the bisimilarity of context-free session types
- Formal methods at the crossroads. From Panacea to foundational support. 10th anniversary colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18--20, 2002. Revised papers
- Generalizing generalized tries
- scientific article; zbMATH DE number 3874579 (Why is no real title available?)
- scientific article; zbMATH DE number 4055576 (Why is no real title available?)
- scientific article; zbMATH DE number 1398002 (Why is no real title available?)
- LALBLC A Program Testing the Equivalence of dpda’s
- Linear logic propositions as session types
- Linear logical relations and observational equivalences for session-based concurrency
- Nested session types
- PARLE 94, Parallel architectures and languages Europe, 6th International PARLE Conference, Athens, Greece, July 4-8, 1994. Proceedings
- Polarized Substructural Session Types
- Propositions as sessions
- Purely Functional Data Structures
- Relating state-based and process-based concurrency through linear logic (full-version)
- Session types as intuitionistic linear propositions
- Session types revisited
- Session Types with Arithmetic Refinements
- Subtyping for session types in the pi calculus
- Talking bananas: structural recursion for session types
- The inclusion problem for simple languages
- Typing copyless message passing
- Work analysis with resource-aware session types
Cited in
(18)- Polymorphic lambda calculus with context-free session types
- Nested session types
- Fairness and communication-based semantics for session-typed languages
- Nested protocols in session types
- Talking bananas: structural recursion for session types
- Context-free session types
- Context-free session type inference
- Bounded polymorphism in session types
- Rast: a language for resource-aware session types
- Behavioral polymorphism and parametricity in session-based communication
- A simple library implementation of binary sessions
- The different shades of infinite session types
- Polarized subtyping
- Polymorphic Session Processes as Morphisms
- Polymorphic higher-order context-free session types
- System \(F^\mu_\omega\) with context-free session types
- Subtyping context-free session types
- Subtyping context-free session types
This page was built for publication: Nested session types
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233456)
