Publications

View publication

Title Aspectual Session Types
Authors Nicolas Tabareau, Mario Südholt, Éric Tanter
Publication date 2014
Abstract Multiparty session types allow the definition of distributed
processes with strong communication safety properties. A global type is a
choreographic specification of the interactions between peers, which is then
projected locally in each peer. Well-typed processes behave accordingly to
the global protocol specification. Multiparty session types are however
monolithic entities that are not amenable to modular extensions. Also,
session types impose conservative requirements to prevent any race
condition, which prohibit the uniform application of extensions at different
points in a protocol. In this paper, we describe a means to support modular
extensions with aspectual session types, a static pointcut/advice mechanism
at the session type level. To support the modular definition of crosscutting
concerns, we augment the expressivity of session types to allow harmless
race conditions. We formally prove that well-formed aspectual session types
entail communication safety. As a result, aspectual session types make
multiparty session types more flexible, modular, and extensible.
Downloaded 5 times
Pages 193-204
Conference name International Conference on Aspect-Oriented Software Development
Publisher ACM Press (New York, NY, USA)
PDF View PDF
Reference URL View reference page