Ensuring that message-passing systems interact according to an intended protocol is a challenging problem, particularly for systems with some reactive or timed components. To rise to this challenge, we study the integration of session-based concurrency and Synchronous Reactive Programming (SRP). We propose MRS, a new process calculus for multiparty sessions enriched with features from SRP. In MRS, protocol participants may broadcast messages, suspend themselves while waiting for a message, and react to events. Our main contribution is a session type system for MRS, which enforces session correctness (protocol conformance) and additionally ensures input timeliness, a time-related property that entails livelock-freedom. As a result, our type system departs significantly from existing ones, specifically as it captures the notion of “logical instant” typical of SRP.
Slides (ST30.pdf) | 2.86MiB |
Sun 22 OctDisplayed time zone: Lisbon change
14:00 - 15:30 | |||
14:00 30mTalk | CAPABLE: A Mechanised Imperative Language with Native Multiparty Session TypesCancelled ST30 Jan de Muijnck-Hughes University of Strathclyde, Cristian Urlea , Adriana Laura Voinea , Wim Vanderbauwhede University of Glasgow | ||
14:30 30mTalk | Complete Multiparty Session Type Projection with Automata ST30 | ||
15:00 30mTalk | Multiparty Reactive Sessions ST30 Ilaria Castellani INRIA Sophia Antipolis, France, Cinzia Di Giusto Université Côte d'Azur; CNRS, Jorge A. Pérez University of Groningen Link to publication File Attached |