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.
Sun 22 OctDisplayed time zone: Lisbon change
14:00 - 15:30
|CAPABLE: A Mechanised Imperative Language with Native Multiparty Session TypesCancelled|
|Complete Multiparty Session Type Projection with Automata|
|Multiparty Reactive Sessions|
Ilaria Castellani INRIA Sophia Antipolis, France, Cinzia Di Giusto Université Côte d'Azur; CNRS, Jorge A. Pérez University of GroningenLink to publication File Attached