Back to Search
Start Over
Minimal session types for the π-calculus.
- Source :
-
Information & Computation . Mar2024, Vol. 297, pN.PAG-N.PAG. 1p. - Publication Year :
- 2024
-
Abstract
- Session types are a type-based approach to correct message-passing programs. A session type specifies a channel's protocol as sequences of exchanges. Aiming to uncover the essential notions of session-based concurrency, prior work defined minimal session types (MSTs), a formulation of session types without the sequentiality construct, and showed a minimality result : every process typable with standard session types can be transformed into a process typable using MSTs. Such a minimality result was proven for a higher-order session π -calculus, in which values are abstractions (functions from names to processes). In this paper, we study MSTs but now for the session π -calculus, the (first-order) language in which values are names and for which session types have been more widely studied. We first show that a new minimality result can be obtained by composing known results. Then, we develop optimizations of this new minimality result and prove also a dynamic correctness guarantee. [ABSTRACT FROM AUTHOR]
- Subjects :
- *FUNCTIONAL analysis
*DIRICHLET principle
*LANGUAGE & languages
Subjects
Details
- Language :
- English
- ISSN :
- 08905401
- Volume :
- 297
- Database :
- Academic Search Index
- Journal :
- Information & Computation
- Publication Type :
- Academic Journal
- Accession number :
- 176010144
- Full Text :
- https://doi.org/10.1016/j.ic.2024.105148