A Minimal Formulation of Session Types: The Sessions of Trios in Concert
Alen Arslanagi\'c, Jorge A. P\'erez, Dan Frumin

TL;DR
This paper introduces minimal session types, demonstrating that complex sequencing in session types can be replaced by sequencing in processes without losing behavioral correctness, simplifying the theoretical framework.
Contribution
It proves that standard session types can be reduced to minimal session types through compilation, maintaining behavioral equivalence, thus simplifying session type systems.
Findings
Every process typable with standard session types can be compiled into a process with minimal session types.
The compiled process is behaviorally equivalent to the original process.
Minimal session types are supported by static and dynamic correctness results.
Abstract
Session types are a type-based approach to the verification of message-passing programs. They specify communication structures essential to enforcing program correctness; by relying on sequencing constructs, a session type can precisely describe the intended order of communication actions through a channel. In this paper we study a fragment of session types that makes a very limited use of sequencing; we call it minimal session types. In the context of a core process calculus with sessions and higher-order concurrency, we establish two technical results. First, we prove that every process P typable with standard session types can be compiled down into a process D(P) typable with minimal session types. Second, we prove that P and D(P) are behaviorally equivalent. These results show that having sequencing in both processes and session types is convenient, but that only sequencing in…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Model-Driven Software Engineering Techniques
