Session types are a type-based approach to the verification of message-passing programs. They have been much studied as type systems for the π-calculus and for languages such as Java. A session type specifies what and when should be exchanged through a channel. Central to session-typed languages are constructs in types and processes that specify sequencing in protocols.
Here we study minimal session types, session types without sequencing. This is arguably the simplest form of session types. By relying on a core process calculus with sessions and higher-order concurrency (abstraction passing), we prove that every process typable with usual (non minimal) session types can be compiled down into a process typed with minimal session types. This means that having sequencing constructs in both processes and session types is redundant; only sequentiality in processes is indispensable, as it can precisely codify sequentiality in types.
Our developments draw inspiration from work by Parrow on behavior-preserving decompositions of untyped processes. By casting Parrow’s results in the realm of typed processes, our results reveal a conceptually simple formulation of session types and a principled avenue to the integration of session types into languages without sequencing in types.
Wed 17 Jul Times are displayed in time zone: Greenwich Mean Time : Belfast change
13:30 - 15:10
|Transient Typechecks are (Almost) Free|
Richard RobertsVictoria University of Wellington, Stefan MarrUniversity of Kent, Michael HomerVictoria University of Wellington, James NobleVictoria University of WellingtonDOI Media Attached
|A Typing Discipline for Hardware Interfaces|
Research PapersDOI Media Attached
|Minimal Session Types|
Alen ArslanagićUniversity of Groningen, Jorge A. PérezUniversity of Groningen, The Netherlands, Erik VoogdUniversity of GroningenDOI Media Attached
|Julia's Efficient Algorithm for Subtyping Unions and Covariant Tuples|
Benjamin ChungNortheastern University, Francesco Zappa NardelliInria, Jan VitekNortheastern UniversityDOI Media Attached
|On Satisfiability of Nominal Subtyping with Variance|
Aleksandr MisonizhnikSaint-Petersburg State University, Dmitry MordvinovSaint-Petersburg State University, JetBrains ResearchDOI Media Attached