We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.
Mon 30 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:45 | Concurrency and TypesTechnical Papers at Auditorium M003 Chair(s): João Costa Seco NOVA-LINCS; Nova University of Lisbon | ||
14:00 21mTalk | Contrasting Deadlock-Free Session Processes Technical Papers DOI | ||
14:21 21mTalk | Fair Termination of Asynchronous Binary Sessions Technical Papers Luca Padovani Department of Computer Science and Engineering - Università di Bologna, Gianluigi Zavattaro Department of Computer Science and Engineering - Università di Bologna | ||
14:42 21mTalk | Incremental Computing by Differential Execution Technical Papers | ||
15:03 21mTalk | Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction Technical Papers Dawit Tirore IT University of Copenhagen, Denmark, Jesper Bengtson IT University of Copenhagen, Marco Carbone IT University of Copenhagen | ||
15:24 21mTalk | Validating Persistency Semantics with Memory Hierarchy Timing Attack Technical Papers Vasileios Klimis Queen Mary University of London |