Asynchronous and Synchronous Mixed Sessions
Session types provide a flexible programming style for structuring interaction, and are used to guarantee a safe and consistent composition of distributed processes. Traditional session types include only one-directional input (external) and output (internal) guarded choices. This prevents the session-processes to explore the full expressive power of the pi-calculus where the mixed choices are proved more expressive than the (non-mixed) guarded choices. To account this issue, recently Casal, Mordido, and Vasconcelos proposed the binary session types with mixed choices (CMV+). Our recent paper at EXPRESS/SOS’22 carries a surprising result on (CMV+): in spite of an inclusion of unrestricted channels with mixed choice, CMV+’s mixed choice is rather separate and not mixed.
In this talk, we present our recent trial to carry out this expressive study for asynchronous mixed sessions (synchronous calculus with FIFO queues) where a naive extension of synchronous mixed sessions breaks the type and communication safety.
Mon 23 OctDisplayed time zone: Lisbon change
11:00 - 12:30
|Asynchronous and Synchronous Mixed Sessions
|Classical Processes in modern dress
|Labelled Tensor Types in Session Based ProgrammingCancelled
Luís Caires INESC-ID / Instituto Superior Tecnico, University of Lisbon